8000 Phase 6b: deterministic MathCorpus and MCIP export by Mnehmos · Pull Request #55 · Mnehmos/MathOS · GitHub
[go: up one dir, main page]
Skip to content

Phase 6b: deterministic MathCorpus and MCIP export - #55

Merged
Mnehmos merged 1 commit into
mainfrom
feat/54-mathcorpus-mcip-export
Jul 22, 2026
Merged

Phase 6b: deterministic MathCorpus and MCIP export#55
Mnehmos merged 1 commit into
mainfrom
feat/54-mathcorpus-mcip-export

Conversation

@Mnehmos
@Mnehmos Mnehmos commented Jul 22, 2026
Copy link
Copy Markdown
Owner

Summary

  • vendor the byte-exact Apache-2.0 MathCorpus packet and MCIP v1 schemas at upstream commit a0d08c9ace0dcc70a8bc281dcf29c560242075d3
  • add the closed corpus_export_manifest/1 contract plus deterministic no-write export, immutable materialization, and database-independent verification by exact source reprojection
  • preserve authority separation with private_audit_only/private_only output for private releases and quarantined output plus explicit public policy requirements for public releases
  • extend protected Pilot A to build, copy, verify, and retain the corpus export while SQLite is hidden
  • record ADR-0012, trust guidance, schema provenance, CLI instructions, and implementation evidence

Validation

  • cargo fmt --all -- --check
  • cargo clippy --workspace --all-targets --all-features -- -D warnings
  • cargo test --workspace --all-targets (156 library, 17 CLI, 4 MCP)
  • opt-in real Lean 4.32.0 integration
  • 39 legacy Python tests
  • actionlint 1.7.12 and bash syntax for the modified Pilot A release script
  • retained Pilot A source release 0417d31249de47d49609913e79021b6a8ba9ec265105a057a29237337c30913d projected deterministically to export 33e6ccc24979e85c14688d755130ace9960f0e074342695e951ac9756c2c590b
  • offline verification passed from a nonexistent instance root; upstream packet and MCIP validators reported zero errors and zero warnings with hash checks enabled

Protected merged-tree evidence and independent downloaded-artifact audit remain required before the issue is closed.

Closes #54

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

Warning

Review limit reached

@Mnehmos, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 24 minutes

Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available.
You're only billed for reviews past your plan's rate limits ($0.25/file).

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details
⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 19baf6b9-489d-43d5-ac3e-0ef95c9cefaa

📥 Commits

Reviewing files that changed from the base of the PR and between 84987c7 and 5571178.

⛔ Files ignored due to path filters (1)
  • Cargo.lock is excluded by !**/*.lock
📒 Files selected for processing (26)
  • .gitattributes
  • .github/workflows/publication.yml
  • Cargo.toml
  • README.md
  • docs/decisions/ADR-0012-deterministic-offline-mathcorpus-mcip-projection.md
  • docs/implementation/BLOCKERS.md
  • docs/implementation/CORPUS_EXPORT.md
  • docs/implementation/RELEASE_CHECKLIST.md
  • docs/implementation/STATUS.md
  • docs/trust/RELEASES.md
  • schemas/mathcorpus/UPSTREAM.md
  • schemas/mathcorpus/upstream-a0d08c9ace0dcc70a8bc281dcf29c560242075d3/LICENSE
  • schemas/mathcorpus/upstream-a0d08c9ace0dcc70a8bc281dcf29c560242075d3/packet.schema.json
  • schemas/mcip/v1/upstream-a0d08c9ace0dcc70a8bc281dcf29c560242075d3/_defs.schema.json
  • schemas/mcip/v1/upstream-a0d08c9ace0dcc70a8bc281dcf29c560242075d3/bundle.schema.json
  • schemas/mcip/v1/upstream-a0d08c9ace0dcc70a8bc281dcf29c560242075d3/dependency_manifest.schema.json
  • schemas/mcip/v1/upstream-a0d08c9ace0dcc70a8bc281dcf29c560242075d3/packet_identity.schema.json
  • schemas/mcip/v1/upstream-a0d08c9ace0dcc70a8bc281dcf29c560242075d3/proof_variant.schema.json
  • schemas/release/corpus-export-manifest-1.schema.json
  • scripts/release-pilot-a.sh
  • src/cli/mod.rs
  • src/corpus_export.rs
  • src/domain/corpus.rs
  • src/domain/mod.rs
  • src/lib.rs
  • tests/phase1_cli.rs
✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/54-mathcorpus-mcip-export

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 marked this pull request as ready for review July 22, 2026 02:08
@Mnehmos
Mnehmos merged commit 8E7A e977d7e into main Jul 22, 2026
6 checks passed
This was referenced Jul 22, 2026
Merged
Closed
Open
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.

Phase 6b: deterministic MathCorpus and MCIP export

1 participant

@Mnehmos
0