Repository navigation
feat: establish verifier-gated zero-to-one slice - #2
Conversation
|
Warning Review limit reached
Next review available in: 31 minutes Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available. How can I continue?After more reviews become available, a review can be triggered using the 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 configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (17)
📝 WalkthroughWalkthroughMathOS adds a trusted claim-verification vertical slice with finite-domain proof search, independent verification, SQLite provenance, trajectory exports, CLI and MCP interfaces, packaging metadata, adversarial tests, documentation, and CI validation. ChangesTrusted claim lifecycle
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant Client
participant CLI_or_MCP
participant ClaimEngine
participant FiniteSearchEngine
participant FiniteDomainVerifier
participant ProvenanceLedger
participant TrajectoryValidator
Client->>CLI_or_MCP: Submit claim
CLI_or_MCP->>ClaimEngine: submit(...)
ClaimEngine->>ProvenanceLedger: persist claim.submitted
Client->>CLI_or_MCP: Run claim
CLI_or_MCP->>ClaimEngine: process(...)
ClaimEngine->>FiniteSearchEngine: search formal specification
FiniteSearchEngine-->>ClaimEngine: candidate certificate
ClaimEngine->>FiniteDomainVerifier: verify candidate
FiniteDomainVerifier-->>ClaimEngine: verification result
ClaimEngine->>ProvenanceLedger: persist status and evidence events
Client->>CLI_or_MCP: Export and validate trajectory
CLI_or_MCP->>ClaimEngine: export_trajectory(...)
ClaimEngine->>TrajectoryValidator: verify_trajectory(...)
TrajectoryValidator-->>Client: valid trajectory result
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches🧪 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 |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a6034df02e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
@codex review Both P1 findings from the prior review are fixed with regression tests. Please review the current head, |
|
@coderabbitai review Please review the current head, |
|
✅ Action performedReview finished.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2f98353da9
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (3)
.github/workflows/ci.yml (1)
20-20: 🔒 Security & Privacy | 🔵 Trivial | ⚡ Quick winPrevent credential persistence in the checkout action.
By default,
actions/checkoutstores theGITHUB_TOKENin the local Git configuration. Since this workflow only runs tests and builds without pushing changes back to the repository, you should disable this behavior to minimize security risks (such as accidental leakage if.gitfiles are included in future artifacts).🛡️ Proposed fix to limit credential persistence
- - uses: actions/checkout@v4 + - uses: actions/checkout@v4 + with: + persist-credentials: false🤖 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/ci.yml at line 20, Update the actions/checkout@v4 step to disable credential persistence by setting persist-credentials to false. Keep the existing checkout behavior unchanged otherwise.Source: Linters/SAST tools
tests/test_cli.py (1)
20-34: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueReuse
run_clihelper instead of duplicating the subprocess call.This block reimplements the same
subprocess.runinvocation asrun_cli(lines 11-17); using the helper avoids drift between the two call sites.♻️ Proposed refactor
def test_demo_runs_complete_vertical_slice(self) -> None: with tempfile.TemporaryDirectory() as directory: - completed = subprocess.run( - [ - sys.executable, - "-m", - "mathos", - "demo", - "--workspace", - directory, - "--reset", - ], - check=True, - capture_output=True, - text=True, - ) - result = json.loads(completed.stdout) + result = self.run_cli("demo", "--workspace", directory, "--reset")🤖 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 `@tests/test_cli.py` around lines 20 - 34, Replace the duplicated subprocess.run invocation in the demo test with the existing run_cli helper, passing the same CLI arguments and workspace directory. Preserve the current check, output capture, and text behavior provided by the helper.tests/test_mcp.py (1)
24-30: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueExtract shared server spawn/teardown into a helper.
Both tests duplicate the same
subprocess.Popensetup andfinallyteardown (terminate/wait/close streams). A small helper (context manager orsetUp/tearDown) would remove the duplication.Also applies to: 145-157, 136-142, 180-186
🤖 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 `@tests/test_mcp.py` around lines 24 - 30, Extract the duplicated MCP server lifecycle from the affected tests into a shared helper, such as a context manager, covering the subprocess.Popen configuration and terminate/wait/stream-close teardown. Update each test’s setup and cleanup to use this helper while preserving the existing server arguments and cleanup behavior.
🤖 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.
Inline comments:
In `@src/mathos/engine.py`:
- Around line 47-54: Handle deterministic duplicate claims across all submission
interfaces: in src/mathos/engine.py lines 47-54, update ClaimEngine.submit() to
catch the ledger collision from insert_claim and raise a clear ValueError or
make identical submissions idempotent; in src/mathos/cli.py lines 124-126,
include sqlite3.Error in main()’s handled exceptions; and in
src/mathos/mcp_server.py lines 197-201, include sqlite3.Error in _call_tool’s
handled exceptions so both interfaces return their structured error responses.
In `@src/mathos/lean.py`:
- Around line 43-49: Wrap the subprocess.run call in the verification flow
around completed so subprocess.TimeoutExpired and OSError are caught, then
return or construct VerificationOutcome.UNKNOWN consistently with the adapter’s
fail-closed behavior. Preserve normal completed-process handling and avoid
allowing execution failures to propagate to callers.
In `@src/mathos/ledger.py`:
- Around line 92-145: Move the existing-claim lookup in insert_claim inside the
BEGIN IMMEDIATE transaction, or catch a concurrent INSERT constraint failure and
reconcile it by reloading the stored claim. Return the existing claim when its
informal_statement and formal_spec match, and raise ValueError("claim identifier
collision") when they differ; do not expose a raw sqlite3.IntegrityError, while
preserving rollback behavior for other failures.
In `@src/mathos/trajectory.py`:
- Around line 47-70: The trajectory verification loop around previous_sequence
and event_hash must also validate the chain linkage: require the first event’s
previous_hash to be None and each subsequent event’s previous_hash to equal the
prior event_hash. Track the prior hash while iterating and return the existing
invalid-event verification failure when the linkage is incorrect.
---
Nitpick comments:
In @.github/workflows/ci.yml:
- Line 20: Update the actions/checkout@v4 step to disable credential persistence
by setting persist-credentials to false. Keep the existing checkout behavior
unchanged otherwise.
In `@tests/test_cli.py`:
- Around line 20-34: Replace the duplicated subprocess.run invocation in the
demo test with the existing run_cli helper, passing the same CLI arguments and
workspace directory. Preserve the current check, output capture, and text
behavior provided by the helper.
In `@tests/test_mcp.py`:
- Around line 24-30: Extract the duplicated MCP server lifecycle from the
affected tests into a shared helper, such as a context manager, covering the
subprocess.Popen configuration and terminate/wait/stream-close teardown. Update
each test’s setup and cleanup to use this helper while preserving the existing
server arguments and cleanup behavior.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 1d95350b-bb5d-491e-bed4-a9f25a27a1d2
📒 Files selected for processing (38)
.github/workflows/ci.yml.gitignoreMakefileREADME.mddocs/architecture/SYSTEM_OVERVIEW.mddocs/architecture/TRUST_MODEL.mddocs/architecture/adr/0001-finite-verifier-first.mddocs/dev-diary/0001-trust-before-scale.mddocs/dev-diary/0002-a-history-that-can-disagree.mddocs/dev-diary/README.mddocs/implementation/0001-zero-to-one-evidence.mddocs/product/SPEC.mddocs/product/ZERO_TO_ONE_DOD.mdexamples/finite/excluded_middle.jsonpyproject.tomlsrc/mathos/__init__.pysrc/mathos/__main__.pysrc/mathos/canonical.pysrc/mathos/cli.pysrc/mathos/demo.pysrc/mathos/engine.pysrc/mathos/finite.pysrc/mathos/lean.pysrc/mathos/ledger.pysrc/mathos/mcp_server.pysrc/mathos/models.pysrc/mathos/pedagogy.pysrc/mathos/trajectory.pytests/__init__.pytests/fixtures/disproved.jsontests/fixtures/proved.jsontests/fixtures/unresolved.jsontests/helpers.pytests/test_adversarial.pytests/test_claim_engine.pytests/test_cli.pytests/test_finite_verifier.pytests/test_mcp.py
Summary
Establish the first complete MathOS claim lifecycle across ingestion, finite formalization, untrusted proof search, verifier-gated outcomes, certainty-preserving pedagogy, tamper-evident provenance, CLI and MCP interfaces, and validated RL trajectory export.
MathOS remains the product. MCP is one interface. MnehmosAI is the company and publishing vehicle.
Change class
Class 3: release and verifier-critical trust-boundary work.
Affected boundaries: claim state transitions, finite verification, counterexample validation, provenance replay, trajectory evidence, CLI, and MCP stdio.
TDD evidence
The initial collection run failed with
ModuleNotFoundError: mathos, establishing Red before the package existed. A later hardening Red run exposed five missing guarantees: materialized-state replay, complete RL lifecycle validation, terminal-only export, bounded integer growth, and bounded statement input. Those tests failed for the intended reasons before implementation and now pass.Verification
Local results:
ResourceWarningpromoted to an errorpip checkProvenance and dependencies
The runtime is Python standard library only. No third-party code or data is introduced. Canonical fixtures and generated demo artifacts are repository-authored. Local demonstration databases and exports are ignored.
Known limitations
These limits are explicit in
docs/architecture/TRUST_MODEL.md.Recovery
Revert this single commit. The release introduces no remote service, migration, or persistent production data.
Definition of Done
Local and GitHub Actions evidence is complete. All eight review threads are resolved, CodeRabbit passes, and the verified branch was squash-merged to
mainas4d51e535e17436e00feb9282bf6de9c8c07b40d0. The remaining release-administration gate is the remotev0.1.0tag on that exact commit.Summary by CodeRabbit
New Features
Documentation
Tests