Repository navigation
feat: add deterministic Comparator-ready package boundary - #61
Merged
Merged
Conversation
📝 WalkthroughWalkthroughThis change adds Comparator-ready package contracts, deterministic five-file export and verification, CLI commands, Pilot A automation, a Lean challenge fixture, schemas, tests, and documentation describing the ready-state trust boundary. ChangesComparator package workflow
Estimated code review effort: 5 (Critical) | ~120 minutes Possibly related issues
Possibly related PRs
Sequence Diagram(s)sequenceDiagram
participant PilotA
participant MCL
participant FrozenRelease
participant ComparatorPackage
PilotA->>MCL: export-comparator
MCL->>FrozenRelease: load and verify release
FrozenRelease-->>MCL: verified release members
MCL->>ComparatorPackage: write deterministic five-file package
PilotA->>MCL: verify-comparator-package
MCL->>ComparatorPackage: verify hashes and inventory
MCL->>FrozenRelease: reproject package inputs
MCL-->>PilotA: verification report
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 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 |
Mnehmos
marked this pull request as ready for review
July 22, 2026 05:04
This was referenced Jul 22, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Tracks #60. Issue #60 intentionally remains open until merged-tree protected evidence is audited. ## Summary Adds a deterministic, offline boundary that projects one verified frozen release into exactly
Challenge.lean,Solution.lean,config.json,formalization.yaml, andverification.json. The package is independently reproducible and can encode onlyready,comparator_verified: false, andauthoritative: false. ## Change class Select one: - [ ] Class 0: Administrative or documentation - [ ] Class 1: Standard implementation - [ ] Class 2: Verifier-critical - [x] Class 3: Release, migration, or security-sensitive Affected trust boundary: portable-release projection into official Comparator input shape. Construction and reprojection establish package integrity only; they do not execute Comparator, create evidence, or grant mathematical authority. ## TDD evidence - [x] Acceptance criteria were defined before implementation - [ ] A focused test or formal obligation failed first for the expected reason - [x] The smallest coherent implementation made it pass - [x] Refactoring preserved passing behavior - [x] Relevant unit and integration suites pass - [x] Failure paths and boundary cases are covered - [ ] Documentation-only exception applies and is explained below Red evidence: issue #60 defined the closed contracts and adversarial acceptance criteria before implementation; no separate retained red-run artifact is claimed. Green evidence: 176 library tests, 19 CLI tests, four MCP tests, the opt-in real Lean integration, and 39 Python regressions pass. Comparator tests cover canonicality, deterministic five-file projection, authority constants, stale inputs, substitution, inventory/tamper, trusted hashes, immutable output, schemas, malformed fields/names/pins, and oversized inputs. Commands and results: -cargo fmt --all -- --check— pass -cargo clippy --workspace --all-targets --all-features -- -D warnings— pass -cargo test --workspace --all-targets— pass -MCL_RUN_LEAN_INTEGRATION=1 cargo test --test lean_worker -- --nocapture— pass -PYTHONPATH=src PYTHONWARNINGS=error::ResourceWarning python -m unittest discover -s tests -v— 39 pass -bash -n scripts/release-pilot-a.sh— pass - Actionlint 1.7.12 — pass -git diff --check— pass - exact-head CI run29893380402— all five jobs pass on36ae9586dc7985785501474c53e1ee3d6067b5f5## Mathematical verification - [ ] No mathemat 8000 ical trust boundary is affected - [x] Candidate output was checked independently from its generator - [x] Formal proof passes the pinned kernel or checker - [ ] Counterexample premises and violated conclusion were checked - [x] Assumptions, domains, tolerances, and dependency pins are recorded - [x] Claim, theorem, witness, or artifact identifiers are linked Verifier and result: offlineverify-comparator-packagereproduced the local five-file Pilot A package from downloaded protected release manifest47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567with verification hashec36212e00e255de770109a44e5bdce2e0e4922491f1a5ae950f93e6ad50ecae; both Lean files elaborate with Lean 4.32.0. The challenge contains an intentionalsorry, and neither result is represented as Comparator verification. ## Provenance and licensing - [x] No new third-party code, data, model output, or dependency - [ ] New third-party material has source, license, and attribution recorded - [x] Generated artifacts include tool, version, configuration, seed, and hash as applicable - [x] MathCorpus and RL export implications are documented - [x] No credentials, private data, or access-controlled material are included Provenance references: official repository/full-commit pins are Comparator68a064109f01c08f47c8edc9f51d6a2bbffaa188, lean4exportaf5aa64bb914c3c2c781f378088dbd38acf4f804, and landrun5ed4a3db3a4ad930d577215c6b9abaa19df7f99f.Solution.leanis copied byte-for-byte from the frozen MathOS release replay member; the Pilot A challenge is repository-owned source. ## Risk and recovery Known limitations: this PR prepares package inputs only. It does not establish challenge/solution equivalence, run the real Linux sandbox, ingest Comparator evidence, change research status, or complete Pilot C. Rollback or recovery plan: revert the implementation commit and publication workflow addition. Existing release, corpus, and RL artifact identities remain independently bound and valid; no schema migration or database write is introduced. Follow-up work: after merged-tree protected artifact audit, implement real pinned Linux Comparator execution and controlled evidence ingestion, then continue the BH Pilot C lifecycle. ## Review readiness - [x] The branch is current with main - [x] The pull request addresses one coherent concern - [x] Required checks pass - [x] Review threads are resolved - [x] I have not represented generated output as independently verified evidence