Mnehmos · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026
@@ -18,6 +18,10 @@ jobs:
     if: github.ref == 'refs/heads/main'
     runs-on: ubuntu-latest
     timeout-minutes: 20
+    outputs:
+      comparator_package_hash: ${{ steps.comparator_bindings.outputs.comparator_package_hash }}
+      comparator_release_hash: ${{ steps.comparator_bindings.outputs.comparator_release_hash }}
+      comparator_plan_hash: ${{ steps.comparator_bindings.outputs.comparator_plan_hash }}
     permissions:
       contents: read
       id-token: write
@@ -193,6 +197,17 @@ jobs:
             "${RUNNER_TEMP}/pilot-a-mathcorpus-mcip-export" \
             "${RUNNER_TEMP}/pilot-a-rl-evaluation-export" \
             "${RUNNER_TEMP}/pilot-a-comparator-package"
+      - name: Bind exact same-run Comparator inputs for the fresh job
+        id: comparator_bindings
+        shell: bash
+        run: |
+          set -euo pipefail
+          package_hash="$(sha256sum "${RUNNER_TEMP}/pilot-a-comparator-package/verification.json" | cut -d ' ' -f 1)"
+          release_hash="$(sha256sum "${RUNNER_TEMP}/pilot-a-portable-release/manifest.json" | cut -d ' ' -f 1)"
+          plan_hash="$(sha256sum "${RUNNER_TEMP}/publication-candidate/release-build-evidence/comparator-package-plan.json" | cut -d ' ' -f 1)"
+          printf 'comparator_package_hash=%s\n' "$package_hash" >> "${GITHUB_OUTPUT}"
+          printf 'comparator_release_hash=%s\n' "$release_hash" >> "${GITHUB_OUTPUT}"
+          printf 'comparator_plan_hash=%s\n' "$plan_hash" >> "${GITHUB_OUTPUT}"
       - name: Retain smoke, candidate closures, release, exports, Comparator package, diagnostics, and Sigstore bundles
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
@@ -223,3 +238,121 @@ jobs:
             ${{ runner.temp }}/pilot-a-mathcorpus-mcip-export/
             ${{ runner.temp }}/pilot-a-rl-evaluation-export/
             ${{ runner.temp }}/pilot-a-comparator-package/
+
+  comparator:
+    name: Protected official Comparator execution
+    needs: boundary
+    if: github.ref == 'refs/heads/main'
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    permissions:
+      actions: read
+      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
+        env:
+          COMPARATOR_RUNNER_ENVIRONMENT: ${{ runner.environment }}
+        run: |
+          set -euo pipefail
+          [[ "${GITHUB_REF_PROTECTED:-}" == "true" \
+            && "${GITHUB_REF}" == "refs/heads/main" \
+            && "${COMPARATOR_RUNNER_ENVIRONMENT}" == "github-hosted" ]] || {
+            echo "official Comparator execution requires protected main on a GitHub-hosted runner" >&2
+            exit 65
+          }
+      - name: Install repository-pinned Lean
+        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 "$(cat lean-toolchain)"
+      - name: Install the pinned landrun build toolchain
+        uses: actions/setup-go@b7ad1dad31e06c5925ef5d2fc7ad053ef454303e
+        with:
+          go-version: "1.24.2"
+          cache: false
+      - name: Build the reviewed offline verifier
+        shell: bash
+        run: cargo build --locked --bin mcl
+      - name: Download the exact successful same-run boundary
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
+        with:
+          name: publication-boundary-${{ github.sha }}
+          path: ${{ runner.temp }}/publication-boundary
+      - 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: Reproject and run the official Comparator in the fresh protected job
+        shell: bash
+        env:
+          COMPARATOR_RUNNER_ENVIRONMENT: ${{ runner.environment }}
+          COMPARATOR_PACKAGE_HASH: ${{ needs.boundary.outputs.comparator_package_hash }}
+          COMPARATOR_RELEASE_HASH: ${{ needs.boundary.outputs.comparator_release_hash }}
+          COMPARATOR_PLAN_HASH: ${{ needs.boundary.outputs.comparator_plan_hash }}
+        run: |
+          bash scripts/comparator-protected-run.sh \
+            "${RUNNER_TEMP}/publication-boundary" \
+            "${COMPARATOR_PACKAGE_HASH}" \
+            "${COMPARATOR_RELEASE_HASH}" \
+            "${COMPARATOR_PLAN_HASH}" \
+            "${RUNNER_TEMP}/comparator-run"
+      - name: Attest the exact canonical Comparator report
+        id: attest_comparator
+        uses: actions/attest@59d89421af93a897026c735860bf21b6eb4f7b26
+        with:
+          subject-path: ${{ runner.temp }}/comparator-run/bundle/report.json
+      - name: Verify the exact protected Comparator attestation
+        shell: bash
+        env:
+          PUBLICATION_GH_BIN: ${{ runner.temp }}/gh_2.96.0_linux_amd64/bin/gh
+              COMPARATOR_BUNDLE_PATH: ${{ steps.attest_comparator.outputs.bundle-path }}
+        run: |
+          scripts/publication-attestation-verify.sh \
+            "${RUNNER_TEMP}/comparator-run/bundle/report.json" \
+            "${COMPARATOR_BUNDLE_PATH}" \
+            "${RUNNER_TEMP}/comparator-run-attestation-verification"
+      - name: Retain the package, report, binaries, raw logs, verifier result, and attestation
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: comparator-run-${{ github.sha }}
+          if-no-files-found: error
+          retention-days: 90
+          compression-level: 6
+          path: |
+            ${{ runner.temp }}/comparator-run/bundle/
+            ${{ runner.temp }}/comparator-run/offline-verification.json
+            ${{ runner.temp }}/comparator-run/report.sha256
+            ${{ runner.temp }}/comparator-run/work/lake-manifest-init.stdout
+            ${{ runner.temp }}/comparator-run/work/lake-manifest-init.stderr
+            ${{ runner.temp }}/comparator-run-attestation-verification/
+            ${{ steps.attest_comparator.outputs.bundle-path }}
@@ -0,0 +1,93 @@
+# ADR-0015: Official Comparator verification is an attested non-authoritative execution result
+
+Date: 2026-07-22
+
+Status: accepted
+
+## Context
+
+A determinis
8000
tic `ready` package is not proof that official Comparator accepted its solution.
+Comparator's security argument also requires a checking environment that has never compiled the
+solution, the exact reviewed Comparator and lean4export sources, real Landlock enforcement, a
+non-root user, the upstream systemd address-family mitigation, and replay by the matching Lean
+kernel.
+
+Running Comparator after readiness diagnostics in the package-publication job would reuse an
+environment that already elaborated `Solution.lean`. Treating an exit code, mutable tool checkout,
+or caller-written JSON as evidence would not preserve the operational assumptions.
+
+## Decision
+
+The publication workflow runs official Comparator only in a separate GitHub-hosted Linux job that
+depends on a successful protected-main boundary job. The boundary job exports trusted hashes for
+the package verification, release manifest, and package plan. The fresh job downloads that exact
+same-run artifact and runs `mcl release verify-comparator-package` against all three identities
+before any solution compilation.
+
+The job builds and retains binaries from these exact source identities:
+
+- Comparator `68a064109f01c08f47c8edc9f51d6a2bbffaa188`, tree
+  `0bb408593d6e5f625db53b3be16e3f1cc91a7524`;
+- lean4export `af5aa64bb914c3c2c781f378088dbd38acf4f804`, tree
+  `5058a7945d24656600ca05917e3c8c174485bcf5`;
+- landrun `5ed4a3db3a4ad930d577215c6b9abaa19df7f99f`, tree
+  `890013a5099a92792cbacd2cfff91af3f13cec9c`.
+
+Comparator and lean4export are built with Lean `v4.32.0`; landrun is built with pinned Go
+`1.24.2`. The report binds those build toolchains as well as the resulting binaries.
+
+Before copying `Challenge.lean`, `Solution.lean`, and `config.json`, the runner creates the
+dependency-free Lake manifest under Lean `v4.32.0`. The resulting harness must have exactly those
+three source files and three runner-owned Lake files, with no `.lake` directory or `.olean` file.
+
+Landrun is first exercised in strict V5 mode without `--best-effort`; failure aborts the run. The
+official Comparator may then use its reviewed `--best-effort` invocation because strict V5 support
+has already been established. Comparator runs as a non-root user in a live user systemd unit with
+`NoNewPrivileges=yes` and `RestrictAddressFamilies=~AF_UNIX`. The unit is held at a runner-owned
+gate outside the harness until those properties and the pristine harness are inspected.
+After the gate opens, a reviewed probe must fail to create an AF_UNIX socket and must fail to
+connect to a live loopback TCP listener through Comparator's exact `--best-effort --ro / --rw
+/dev -ldd -add-exec` landrun base arguments. The report verifier requires one success marker from
+each denial challenge.
+
+The closed canonical `comparator_run_report/1` binds the exact package, reprojection receipt,
+workflow and runner, source commit and tree, tool commits, trees and binaries, harness metadata,
+sandbox predicates, raw output, exit result, and the retained runner script that defines the exact
+invocation. Acceptance requires empty stderr and one ordered instance of each official success
+path marker, including equal challenge/solution export targets and Lean-kernel acceptance.
+
+`mcl release verify-comparator-run` verifies the exact 20-file tree without opening SQLite. It
+streams binary hashes, revalidates the five-file package, checks every report binding, parses the
+Lake and reprojection records, verifies live sandbox records, and independently classifies the raw
+Comparator output. The canonical report is attested and the attestation is verified by the pinned
+GitHub CLI verifier.
+
+An accepted report may set
8BD0
 `comparator_verified: true`. It must set `authoritative: false` and
+cannot create evidence, update research status, or complete Pilot C. Canonical evidence ingestion
+is a separate policy gate.
+
+## Consequences
+
+- Prior solution diagnostics cannot contaminate the official checking environment.
+- Package, plan, release, workflow, runner, tool, harness, sandbox, log, or invocation changes make
+  the report stale or invalid.
+- Failed controls and unexpected output cannot be represented as accepted verification.
+- The retained binaries and runner script permit independent artifact audit without retaining
+  large build trees.
+- Attestation authenticates the protected execution context but does not grant MathOS authority.
+
+## Rejected alternatives
+
+### Run Comparator at the end of the boundary job
+
+Rejected because that job already compiles the solution during readiness checks.
+
+### Trust Comparator's exit code alone
+
+Rejected because exit status does not bind the package, tool binaries, sandbox, runner, output
+path, or workflow identity.
+
+### Let the report promote evidence directly
+
+Rejected because execution authenticity and canonical evidence authority are distinct trust
+transitions.