8000 Exercise the attested publication authority boundary by Mnehmos · Pull Request #22 · Mnehmos/MathOS · GitHub
[go: up one dir, main page]
Skip to content

Exercise the attested publication authority boundary - #22

Merged
Mnehmos merged 12 commits into
mainfrom
feat/publication-proof-authority
Jul 19, 2026
Merged

Exercise the attested publication authority boundary#22
Mnehmos merged 12 commits into
mainfrom
feat/publication-proof-authority

Conversation

@Mnehmos
@Mnehmos Mnehmos commented Jul 19, 2026 •
edited by coderabbitai Bot
Loading
Copy link
Copy Markdown
Owner

Outcome

Adds the first real publication-profile boundary for proof authority. A pinned Lean toolchain checks a committed theorem in a clean Linux job, the verifier runs inside a network-isolated Bubblewrap namespace with an enforced address-space limit, and the workflow retains a hashed candidate report plus diagnostics and an OIDC-backed GitHub artifact attestation.

The report remains explicitly non-authoritative. Canonical promotion is intentionally deferred until the engine independently verifies the attestation and all policy bindings.

Closes part of #21.

Controls

  • clean-checkout enforcement
  • typed, allowlisted Lean invocation
  • Bubblewrap network isolation
  • prlimit memory enforcement
  • pinned action and Lean installer identities
  • retained report, diagnostics, and Sigstore bundle
  • CI smoke coverage of the same boundary

Validation

  • bash -n scripts/publication-smoke.sh
  • git diff --check
  • local Rust and schema suites remained green at the preceding authority-contract checkpoint

The pull request stays draft until the GitHub-hosted Linux boundary passes.

Summary by CodeRabbit

  • New Features

    • Added an isolated publication smoke test for validating Lean execution under restricted resources and filesystem access.
    • Added a signed publication-boundary workflow that generates and retains verification reports and diagnostics.
    • Added a minimal Lean publication theorem used by the smoke test.

  • Documentation

    • Added developer diary entries and updated implementation and trust documentation with publication-boundary status and test details.

@coderabbitai
coderabbitai Bot commented Jul 19, 2026 •
edited
Loading
Copy link
Copy Markdown

Review Change Stack

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 9e38de6b-8adf-4f4a-aacc-3047381cafc4

📥 Commits

Reviewing files that changed from the base of the PR and between 851a578 and 5055815.

📒 Files selected for processing (9)
  • .github/workflows/ci.yml
  • .github/workflows/publication.yml
  • docs/dev-diary/0030-the-smallest-proof-can-test-the-largest-boundary.md
  • docs/dev-diary/0031-a-boundary-must-admit-when-it-is-missing.md
  • docs/dev-diary/README.md
  • docs/implementation/STATUS.md
  • docs/trust/PUBLICATION_AUTHORITY.md
  • fixtures/publication/Smoke.lean
  • scripts/publication-smoke.sh
📝 Walkthrough

Walkthrough

Adds a sandboxed Lean publication smoke test, integrates it into CI and a protected main-branch workflow, attests the generated report, retains evidence, and documents the publication-boundary status.

Changes

Publication boundary validation

Layer / File(s) Summary
Isolated Lean smoke runner
fixtures/publication/Smoke.lean, scripts/publication-smoke.sh		 Adds a trivial Lean theorem and a clean-checkout smoke runner using Bubblewrap, namespace isolation, resource limits, artifact hashing, and JSON invariant validation.
CI and publication authority wiring
.github/workflows/ci.yml, .github/workflows/publication.yml, docs/dev-diary/*, docs/implementation/STATUS.md, docs/trust/PUBLICATION_AUTHORITY.md		 Runs the smoke test in CI and on protected main-branch pushes, attests and uploads its evidence, and updates related documentation and diary indexes.

Estimated code review effort: 4 (Complex) | ~45 minutes

Possibly related issues

  • Issue #21 — The changes implement its publication-boundary smoke test, isolation controls, attestation, and retained evidence.
✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/publication-proof-authority

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.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@Mnehmos Mnehmos mentioned this pull request Jul 19, 2026
Closed
12 tasks done
@Mnehmos ChatGPT Codex Connector
Mnehmos commented Jul 19, 2026
Copy link
Copy Markdown
Owner Author

Adversarial CI found the runner did not contain /usr/bin/bwrap; the boundary failed closed before Lean ran. Commit b9ff79d8c327b129537cb57594f19c816101d552 now provisions Bubblewrap explicitly in both ordinary CI and the protected publication workflow, records its version in the candidate report, and emits stable diagnostics for every missing prerequisite. No isolation requirement was weakened.

Retry tree: 3553f6e2c71e26e9bb1121d82c2c3ad73a8486e6.

@Mnehmos
Mnehmos marked this pull request as ready for review July 19, 2026 23:29
@Mnehmos
Mnehmos merged commit 31ccfdd into main Jul 19, 2026
5 of 6 checks passed
@Mnehmos Mnehmos mentioned this pull request Jul 20, 2026
Open
This was referenced Jul 20, 2026
Merged
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Mnehmos
0