Repository navigation
Produce protected publication candidates - #31
Conversation
📝 WalkthroughWalkthroughThe PR adds a retained-closure contract and protected publication-candidate lifecycle. It implements strict application and CLI validation, creates isolated candidates with bounded Lean execution, updates protected workflows and artifact retention, and documents the resulting authority-boundary requirements. ChangesPublication candidate lifecycle
Estimated code review effort: 5 (Critical) | ~120 minutes Possibly related issues
Possibly related PRs
Sequence Diagram(s)sequenceDiagram
participant ProtectedWorkflow
participant PublicationCandidate
participant LeanSandbox
participant MCL
participant AttestationVerifier
ProtectedWorkflow->>PublicationCandidate: provide protected workflow context
PublicationCandidate->>MCL: prepare request and evidence
PublicationCandidate->>LeanSandbox: execute protected rebuild and audits
LeanSandbox-->>PublicationCandidate: return bounded execution evidence
PublicationCandidate->>MCL: generate and validate retained closure
ProtectedWorkflow->>AttestationVerifier: attest and verify publication report
🚥 Pre-merge checks | ✅ 3 | ❌ 2❌ Failed checks (2 warnings)
✅ Passed checks (3 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
Hosted failure retained before repair:\n\n- CI run: https://github.com/Mnehmos/MathOS/actions/runs/29714982064\n- job: https://github.com/Mnehmos/MathOS/actions/runs/29714982064/job/88266362527\n- exact PR head: 7d4bbdc\n- successful before failure: pinned Lean installation, real local Lean integration, prior isolation smoke, protected candidate rebuild, and protected parser-derived dependency scan\n- failing stage: verifier-controlled ProtectedAudit.lean\n- retained log: libc++abi: terminating due to uncaught exception of type lean::exception: failed to create thread\n- script result: stable exit 70, classified execution_failed\n\nThe four-gibibyte process address-space limit was sufficient for the smaller rebuilds but not the axiom-driver runtime/thread overhead. I am preserving a four-gibibyte Lean heap cap while raising the OS address-space ceiling to six GiB, and adding failed-attempt artifact upload to PR CI. No check is being bypassed and no authority is created. |
|
Second hosted failure retained and inspected:
The memory repair is confirmed: protected rebuild, The remaining failure is a JSON-shape bug after those controls: |
|
Final pre-merge evidence for the exact current head:
The two earlier hosted failures remain documented in this PR and were repaired before this green run. Merge will use an exact-head guard; the protected-main publication artifact will be inspected separately after merge. |
There was a problem hiding this comment.
🧹 Nitpick comments (1)
.github/workflows/publication.yml (1)
120-128: 🔒 Security & Privacy | 🔵 Trivial | ⚡ Quick winPass the attestation bundle path through
envinstead of interpolating${{ }}into the run script.
${{ steps.attest_candidate.outputs.bundle-path }}is expanded directly into the shell body of a step in a job that holdsid-token: writeandattestations: write. Even though this output originates from the trustedactions/atteststep, injecting expression results intorun:is the pattern static analysis flags; binding it to anenvvar and referencing the shell variable removes the interpolation surface. The same pattern also exists (unchanged) at Line 96 for the smoke path.🔒 Proposed hardening
- name: Verify exact candidate attestation and retain the challenge result shell: bash env: PUBLICATION_GH_BIN: ${{ runner.temp }}/gh_2.96.0_linux_amd64/bin/gh + CANDIDATE_BUNDLE_PATH: ${{ steps.attest_candidate.outputs.bundle-path }} run: | scripts/publication-attestation-verify.sh \ "${RUNNER_TEMP}/publication-candidate/publication-report.json" \ - "${{ steps.attest_candidate.outputs.bundle-path }}" \ + "${CANDIDATE_BUNDLE_PATH}" \ "${RUNNER_TEMP}/publication-candidate-attestation-verification"🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In @.github/workflows/publication.yml around lines 120 - 128, Update the attestation verification steps around “Verify exact candidate attestation and retain the challenge result” and the corresponding smoke-path step to pass the attest_candidate bundle-path output through the step’s env block, then reference the shell environment variable in each run script instead of interpolating the GitHub expression directly.Source: Linters/SAST tools
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Nitpick comments:
In @.github/workflows/publication.yml:
- Around line 120-128: Update the attestation verification steps around “Verify
exact candidate attestation and retain the challenge result” and the
corresponding smoke-path step to pass the attest_candidate bundle-path output
through the step’s env block, then reference the shell environment variable in
each run script instead of interpolating the GitHub expression directly.
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 3dad79c0-5a45-4ef9-9c10-767284da61cc
📒 Files selected for processing (18)
.github/workflows/ci.yml.github/workflows/publication.ymldocs/decisions/ADR-0006-oidc-attested-publication-authority.mddocs/dev-diary/0034-a-proof-must-travel-with-its-luggage.mddocs/dev-diary/README.mddocs/implementation/RELEASE_CHECKLIST.mddocs/implementation/STATUS.mddocs/trust/PUBLICATION_AUTHORITY.mdfixtures/environment/lean-4.32-no-imports-local.jsonfixtures/environment/lean-4.32-no-imports-local.sha256schemas/publication/publication-retained-closure-1.schema.jsonscripts/publication-candidate.shsrc/app.rssrc/cli/mod.rssrc/domain/environment.rssrc/domain/mod.rssrc/domain/publication.rstests/phase1_cli.rs
|
Addressed the review hardening in
No review thread was created. The exact new head is now running the full protected check suite. |
|
Exact review-fixed head is green and ready for the guarded merge:
All five required jobs passed; CodeRabbit completed on this head; there are no inline review comments or unresolved conversations. |
|
First protected-main candidate run after merge failed closed and was retained:
The protected-ref workflow gate passed, as did smoke execution, smoke attestation, and the constrained smoke challenge. Candidate construction then exited Root cause: the script's report constant |
|
Protected candidate production is now complete and independently inspected. Exact merged source:
Downloaded candidate audit:
Inspection confirmed exactly 25 sorted fixed-path closure members and all member hashes; source commit/tree/run/attempt agreement; clean checkout; GitHub-hosted protected The report, attempt, validator result, and constrained attestation record all remain |
Outcome
publication_request/1and non-authoritativepublication_report/1from a fresh no-import Lean lifecycle.publication_retained_closure/1with fixed paths, semantic identities, exact byte hashes, local evidence, protected rebuild output, parser-derived dependency output, and axiom-audit output.mcl verify validate-publication-candidate, which replays the retained chain, Store/CAS snapshots, policies, jobs, reports, logs, protected dependencies, and axioms, then dry-run re-derives the request without promotion.Trust-boundary corrections
Security review found that
mainwas not actually protected. Usinggh api, repository protection now requires pull requests, strict passage of all five CI jobs, resolved conversations, stale-review dismissal, and admin enforcement; force-pushes and deletions are disabled. Both the workflow and script also fail unless GitHub reports the main ref as actively protected.Review also found that line-based import detection missed valid Lean forms such as comment-prefixed imports. The candidate now runs pinned Lean
--depsinside Bubblewrap, retains the raw output, clears the inherited environment, and accepts only the implicit pinned/opt/lib/lean/Init.oleanclosure with empty matching manifests.Additional fail-closed fixes cover failed
git status, oversized decimal run identities, symlinked/out-of-root inputs, output-path aliases, wall-clock/memory/output bounds, and structured protected-execution failures.CodeRabbit's final hardening review was addressed by binding both attestation action outputs through step environment variables instead of interpolating them into privileged shell bodies.
Validation
cargo fmt --all -- --checkcargo clippy --workspace --all-targets --all-features -- -D warningscargo test --workspace --all-targets- 102 tests passedMCL_RUN_LEAN_INTEGRATION=1 cargo test --test lean_worker -- --nocapturePYTHONPATH=src PYTHONWARNINGS=error::ResourceWarning python -m unittest discover -s tests -v- 39 tests passedmcl init,mcl health, andmcl doctorgit diff --checkFinal exact-head CI: run
29716143032; all five required jobs passed and CodeRabbit completed.2752340bd32bf5eaef7b9bac10ae7a1fe81bb99c7508582f4ac01b6cd4533c135d7da5f238ad2149b4cb29c908537ad0a46e8df7a24ee09f1c6c2dfac4caee527389958d0c1a558debab4cb3f070e03a706f178079567a6d72a1244b0ba5266fc5c208b961efb64b4ab09b05d81802222dfe17038df8cba51ecbadc8fb40d86eab3030e61da432898530b3582b3cc38c5898cdbd5b06d2687222b6a6authoritative:falseRun
29714982064retained a thread-creation failure under the initial 4 GiB process ceiling. Run29715179869proved the corrected protected rebuild/dependency/axiom path, retained its bounded failed attempt artifact, and exposed a direct-job-snapshot selector error. Both findings were repaired before the green runs.Non-goals
Every report, validation result, attempt record, and attestation-verification record remains
authoritative:false. This PR does not ingest downloaded attestations, create authoritative proof/refutation evidence, or derive mathematical truth status.Advances #21.