Mnehmos · Jul 20, 2026 · Jul 20, 2026 · Jul 20, 2026 · Jul 20, 2026
@@ -113,6 +113,82 @@ jobs:
           export PUBLICATION_SOURCE_TREE_SHA
           PUBLICATION_SOURCE_TREE_SHA="$(git rev-parse 'HEAD^{tree}')"
           bash scripts/publication-candidate.sh "${RUNNER_TEMP}/publication-candidate-simulated-main"
+      - name: Exercise staged-CAS ingestion barrier without authority
+        shell: bash
+        run: |
+          set -euo pipefail
+          candidate="${RUNNER_TEMP}/publication-candidate-simulated-main"
+          bundle="${candidate}/simulated-attestation.json"
+          jq -cS -n '{mediaType:"application/vnd.dev.sigstore.bundle.v0.3+json",verificationMaterial:{},dsseEnvelope:{}}' \
+            | tr -d '\n' >"${bundle}"
+          report_hash="$(sha256sum "${candidate}/publication-report.json" | cut -d ' ' -f 1)"
+          bundle_hash="$(sha256sum "${bundle}" | cut -d ' ' -f 1)"
+          stage_args=(
+            --root "${candidate}" --json verify stage-publication-candidate
+            --report-file publication-report.json
+            --retained-closure-file publication-retained-closure.json
+            --retained-root .
+            --attestation-bundle-file simulated-attestation.json
+            --actor simulated-ci
+            --idempotency-key "simulated-stage:${report_hash}:${bundle_hash}"
+          )
+          target/debug/mcl "${stage_args[@]}" --dry-run >"${RUNNER_TEMP}/stage-dry-run.json"
+          jq -e '.dry_run == true and .stage == null and .authoritative == false' \
+            "${RUNNER_TEMP}/stage-dry-run.json" >/dev/null
+          target/debug/mcl "${stage_args[@]}" >"${RUNNER_TEMP}/stage.json"
+          target/debug/mcl "${stage_args[@]}" >"${RUNNER_TEMP}/stage-retry.json"
+          cmp "${RUNNER_TEMP}/stage.json" "${RUNNER_TEMP}/stage-retry.json"
+          jq -e '.dry_run == false and .stage.stage.authoritative == false and .authoritative == false' \
+            "${RUNNER_TEMP}/stage.json" >/dev/null
+          report_cas="${candidate}/.mcl/artifacts/sha256/${report_hash:0:2}/${report_hash:2:2}/${report_hash}"
+          report_backup="${RUNNER_TEMP}/staged-report.backup"
+          mv "${report_cas}" "${report_backup}"
+          if target/debug/mcl --root "${candidate}" --json verify ingest-publication \
+            --report-artifact-hash "${report_hash}" \
+            --attestation-bundle-artifact-hash "${bundle_hash}" \
+            --actor simulated-ci \
+            --idempotency-key "simulated-ingestion-missing:${report_hash}:${bundle_hash}" \
+            >"${RUNNER_TEMP}/unexpected-missing-ingestion.json" \
+            2>"${RUNNER_TEMP}/expected-missing-ingestion-error.json"; then
+            echo "candidate with a missing staged report crossed the ingestion boundary" >&2
+            exit 1
+          fi
+          jq -e '.code == "MCL_PUBLICATION_STAGE_MEMBER_MISSING"' \
+            "${RUNNER_TEMP}/expected-missing-ingestion-error.json" >/dev/null
+          mv "${report_backup}" "${report_cas}"
+          cp "${report_cas}" "${report_backup}"
+          printf 'altered staged report' >"${report_cas}"
+          if target/debug/mcl --root "${candidate}" --json verify ingest-publication \
+            --report-artifact-hash "${report_hash}" \
+            --attestation-bundle-artifact-hash "${bundle_hash}" \
+            --actor simulated-ci \
+            --idempotency-key "simulated-ingestion-altered:${report_hash}:${bundle_hash}" \
+            >"${RUNNER_TEMP}/unexpected-altered-ingestion.json" \
+            2>"${RUNNER_TEMP}/expected-altered-ingestion-error.json"; then
+            echo "candidate with an altered staged report crossed the ingestion boundary" >&2
+            exit 1
+          fi
+          jq -e '.code == "MCL_PUBLICATION_STAGE_MEMBER_MISMATCH"' \
+            "${RUNNER_TEMP}/expected-altered-ingestion-error.json" >/dev/null
+          mv "${report_backup}" "${report_cas}"
+          fake_bin="${RUNNER_TEMP}/unpinned-publication-verifier"
+          mkdir -p "${fake_bin}"
+          printf '#!/usr/bin/env sh\necho unpinned verifier must never execute >&2\nexit 97\n' >"${fake_bin}/gh"
+          chmod 500 "${fake_bin}/gh"
+          if PATH="${fake_bin}:${PATH}" target/debug/mcl --root "${candidate}" --json verify ingest-publication \
+            --report-artifact-hash "${report_hash}" \
+            --attestation-bundle-artifact-hash "${bundle_hash}" \
+            --actor simulated-ci \
+            --idempotency-key "simulated-ingestion-unpinned:${report_hash}:${bundle_hash}" \
+            >"${RUNNER_TEMP}/unexpected-ingestion.json" \
+            2>"${RUNNER_TEMP}/expected-ingestion-error.json"; then
+            echo "unpinned verifier crossed the ingestion boundary" >&2
+            exit 1
+          fi
+          jq -e '.code == "MCL_PUBLICATION_VERIFIER_PIN_MISMATCH"' \
+            "${RUNNER_TEMP}/expected-ingestion-error.json" >/dev/null
+          target/debug/mcl --root "${candidate}" --json doctor \
+            | jq -e '.healthy == true and ([.checks[] | select(.name == "artifact_inventory" and .healthy == true)] | length) == 1' >/dev/null
       - name: Retain a failed simulated candidate attempt
         if: failure()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02

@@ -128,6 +128,15 @@ jobs:
             "${RUNNER_TEMP}/publication-candidate/publication-report.json" \
             "${CANDIDATE_BUNDLE_PATH}" \
             "${RUNNER_TEMP}/publication-candidate-attestation-verification"
+      - name: Stage and ingest the exact candidate through MathOS
+        shell: bash
+        env:
+          CANDIDATE_BUNDLE_PATH: ${{ steps.attest_candidate.outputs.bundle-path }}
+        run: |
+          scripts/publication-ingest.sh \
+            "${RUNNER_TEMP}/publication-candidate" \
+            "${CANDIDATE_BUNDLE_PATH}" \
+            "${RUNNER_TEMP}/publication-candidate-ingestion"
       - name: Retain smoke, candidate closure, diagnostics, and Sigstore bundles
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
@@ -144,4 +153,5 @@ jobs:
             ${{ runner.temp }}/publication-candidate/publication-retained-closure.json
             ${{ runner.temp }}/publication-candidate/publication-report.json
             ${{ runner.temp }}/publication-candidate-attestation-verification/
+            ${{ runner.temp }}/publication-candidate-ingestion/
             ${{ steps.attest_candidate.outputs.bundle-path }}
@@ -49,7 +49,7 @@ Phase 3 diagnostic evidence: the closed `evidence/1` contract names exact subjec
 
 Phase 3 local audit evidence: the committed audit policy and closed request/report schemas bind an exact formalization, accepted elaboration diagnostic, environment, module, declaration, and policy identity. Durable audit jobs run source escape scans and verifier-controlled `#print axioms`, retain private diagnostics, and atomically promote diagnostic proof-closure and axiom-audit evidence. Policy mismatch, malformed output, duplicate axioms, retries, restart, partial promotion, and corruption fail closed. Local audits explicitly lack publication memory and network isolation and cannot become authoritative, so the complete proof-authority and publication criteria remain unchecked.
 
-Phase 3 publication contract evidence: the closed publication policy, request, retained closure, and candidate report bind exact proof or refutation intent, diagnostic and audit evidence, formalization, environment, module, declaration, Git commit and tree, protected workflow identity, runner class, required isolation controls, retained artifacts, and SHA-pinned attestation actions. The application derives canonical private request artifacts from the current formalization head and one exact accepted elaboration/audit chain without accepting request JSON or authority fields. Typed formalization polarity prevents one exact version/evidence closure from being requested as both proof and refutation; legacy records without polarity cannot publish until versioned and reverified. Transactional head and idempotency checks cover matching preexisting CAS identities. The workflow-facing validator then requires 25 exact fixed-path closure roles, recomputes every member hash, replays the source, claim, formalization, evidence, job, report, policy, environment, module, parser-derived protected dependency output, and local/protected axiom relationships, and dry-run re-derives the request from current Store and CAS state. The protected producer fails unless GitHub reports an actively protected source ref, then builds a real no-import candidate under clean-checkout, Bubblewrap network/process isolation, timeout, memory, and output-size controls; pull-request CI runs it without attestation, while protected `main` attests the exact candidate report. Bounded structured attempt diagnostics and available CAS bytes are retained even when generation fails. Every request, report, validation result, and attestation-verification record remains structurally non-authoritative. Polarity remains intent until combined with reviewed fidelity. Controlled downloaded-closure ingestion and authoritative evidence creation remain incomplete, so every proof-authority criterion remains unchecked.
+Phase 3 publication contract evidence: the closed publication policy, request, retained closure, candidate report, quarantine stage, canonical CAS attestation-verification record (`publication_attestation_verification/1`), and separate immutable SQLite ingestion receipt (`PublicationIngestionReceiptSnapshot` in `publication_ingestion_receipts`) bind exact proof or refutation intent, diagnostic and audit evidence, formalization, environment, module, declaration, Git commit and tree, protected workflow identity, runner class, required isolation controls, retained artifacts, and SHA-pinned attestation actions and verifier. The application derives canonical private request artifacts from the current formalization head and one exact accepted elaboration/audit chain without accepting request JSON or authority fields. Typed formalization polarity prevents one exact version/evidence closure from being requested as both proof and refutation; legacy records without polarity cannot publish until versioned and reverified. The workflow-facing validator and staging path require 25 exact fixed-path closure roles, recompute every member hash, and replay the source, claim, formalization, evidence, job, report, policy, environment, module, parser-derived protected dependency output, and local/protected axiom relationships. Hash-only CLI and MCP ingestion resolve that immutable stage, run an isolated copy of the Linux-amd64 SHA-pinned GitHub CLI with fixed arguments, parse one closed attestation result, retain the raw output and canonical CAS attestation-verification record, then register the separate immutable SQLite ingestion receipt plus the logical stage/actor idempotency result in one final transaction that rechecks currentness. Missing or altered CAS, stale state, key rebinding, parser ambiguity, and unpinned or misbehaving verifiers fail closed. The protected producer fails unless GitHub reports an actively protected source ref, then builds a real no-import candidate under clean-checkout, Bubblewrap network/process isolation, timeout, memory, and output-size controls; pull-request CI runs it without attestation, while protected `main` attests the exact candidate report. Every request, report, stage, validation result, attestation-verification record, and ingestion receipt remains structurally non-authoritative. The attestation-verification record and its ingestion receipt prove provenance only and may not be treated as a passed report or proof; polarity remains intent until combined with reviewed fidelity. Merged-tree ingestion evidence and authoritative evidence creation remain incomplete, so every proof-authority criterion remains unchecked.
 
 Remote evidence: GitHub Actions run `29704542965` passed the exact real Lean audit lifecycle and fresh Linux and Windows suites on tree `30d55d6e2ce7b0de2d921cff3e1368124fd9f66f`. This validates the local diagnostic audit capability only. The verification checklist remains open until publication-profile authority, replay, and retained publication evidence are complete.