Repository navigation
feat: add atomic Pilot A counterexample repair - #45
Conversation
📝 WalkthroughWalkthroughAdds an atomic counterexample-repair workflow with versioned contracts, canonical package hashing, independent repaired claims, controlled lineage edges, shared CLI/MCP access, transaction safeguards, Pilot A integration, tests, and documentation. ChangesCounterexample repair
Estimated code review effort: 5 (Critical) | ~90+ minutes Possibly related issues
Possibly related PRs
🚥 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 |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fec9db8398
ℹ️ 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.
🧹 Nitpick comments (2)
src/domain/counterexample.rs (1)
532-534: 🗄️ Data Integrity & Integration | 🔵 Trivial | 💤 Low valueOptional:
text_schemais more permissive thanvalidate_text.
validate_textrejects whitespace-only strings (value.trim().is_empty()) and bounds by byte length, but the generated schema declaresminLength: 1/maxLength: MAX_TEXT_BYTES, which JSON Schema counts in characters and which admits whitespace-only strings. A payload that passes the committed schema (e.g." ", or a multi-byte string near the limit) can still be rejected by the Rust contract. Since the Rust path is the enforced gate this is not exploitable, but the two representations of the "same" contract diverge. Consider documenting the byte/trim semantics as the authoritative bound.🤖 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 `@src/domain/counterexample.rs` around lines 532 - 534, Align text_schema with validate_text by documenting that the Rust validator’s trimmed, byte-length semantics are authoritative, or adjust the schema representation if the project supports those constraints. Ensure the schema contract does not imply character-based minLength/maxLength validation or acceptance of whitespace-only strings.tests/mcp_stdio.rs (1)
288-338: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winAdd a success-path
counterexampleMCP test.All new
counterexamplecoverage here exercises error paths (missing fields, malformed JSON, unknown artifact, forbiddendry_run). Nothing verifies a successfulrepair/getround trip through the MCP stdio transport itself — that leaves theParameters<CounterexampleRequest>→Application→to_value→CallToolResultwiring for the happy path exercised only indirectly, via the CLI-driven Pilot A script andApplication-layer unit tests, not via MCP.Consider adding one test that runs a fixture through fidelity/authority setup (as the
Applicationtests already do), then callscounterexamplewithaction: "repair"(dry-run and persisted) andaction: "get"over stdio, assertingisError == falseand a few keystructuredContentfields.🤖 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/mcp_stdio.rs` around lines 288 - 338, Extend the existing counterexample MCP stdio test with a successful fixture setup using the same fidelity/authority configuration as the Application tests. Exercise repair in both dry-run and persisted modes, then call get for the persisted result over stdio. Assert each response has isError false and validate key structuredContent fields, including the repaired counterexample and retrieved artifact data.
🤖 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 `@src/domain/counterexample.rs`:
- Around line 532-534: Align text_schema with validate_text by documenting that
the Rust validator’s trimmed, byte-length semantics are authoritative, or adjust
the schema representation if the project supports those constraints. Ensure the
schema contract does not imply character-based minLength/maxLength validation or
acceptance of whitespace-only strings.
In `@tests/mcp_stdio.rs`:
- Around line 288-338: Extend the existing counterexample MCP stdio test with a
successful fixture setup using the same fidelity/authority configuration as the
Application tests. Exercise repair in both dry-run and persisted modes, then
call get for the persisted result over stdio. Assert each response has isError
false and validate key structuredContent fields, including the repaired
counterexample and retrieved artifact data.
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 017e7705-1b3c-4a61-adb5-323171a06420
📒 Files selected for processing (18)
docs/decisions/ADR-0009-atomic-counterexample-package-and-claim-repair.mddocs/dev-diary/0037-a-correction-needs-two-names.mddocs/dev-diary/README.mddocs/implementation/STATUS.mddocs/trust/COUNTEREXAMPLE_REPAIR.mddocs/trust/FIDELITY.mddocs/trust/PUBLICATION_AUTHORITY.mdschemas/counterexample/counterexample-package-1.schema.jsonschemas/counterexample/counterexample-repair-request-1.schema.jsonscripts/publication-ingest.shsrc/app.rssrc/cli/mod.rssrc/domain/counterexample.rssrc/domain/mod.rssrc/mcp/mod.rssrc/store/mod.rstests/mcp_stdio.rstests/phase1_cli.rs
|
Protected merged-tree acceptance is complete. Exact Git identities:
GitHub verification:
Independent downloaded-artifact audit:
This satisfies issue #44. It does not prove the repaired claim or complete Pilot A / MathOS 1.0. The next focused slice is a new formalization, protected proof authority, and role-separated fidelity for the repaired claim without changing the original claim or repair package. |
Closes #44
Summary
Adds the focused Pilot A repair slice: a closed counterexample package, an application-derived and atomically committed repaired claim, a controlled immutable repair edge, shared CLI/MCP access, and protected-workflow retention. The original false claim remains independently addressable and
disproved; the repaired claim startsnot_started.Review follow-up
a255608additionally requires an exact matchingcounterexample_search_result/1observation, preserves retries after later run events, and rejects any MCPdry_runfield on the read action.Change class
Select one:
Affected trust boundary: derived claim status, receipt-bound refutation reuse, counterexample provenance, canonical CAS packaging, and atomic immutable claim lineage. This path packages already revalidated evidence; it cannot create proof or refutation authority.
TDD evidence
Red evidence: issue #44 defined the closed package, atomicity, immutability, retry, concurrency, and interface obligations before the capability existed. Review then exposed three focused failing obligations: a start-only run was accepted, later run events blocked retry, and MCP
getaccepteddry_run:false.Green evidence: the domain/application/store/CLI/MCP tests cover canonical identity, dry-run, rollback injection, concurrency, restart, idempotency rebinding, CAS corruption, start-only and mismatched search results, post-repair run extension, generic-edge denial, and forbidden MCP fields.
Commands and results:
cargo fmt --check- passcargo clippy --workspace --all-targets --all-features -- -D warnings- passcargo test --workspace- pass (140 unit, 12 CLI integration, 3 MCP integration, Lean worker baseline)MCL_RUN_LEAN_INTEGRATION=1 cargo test --test lean_worker -- --nocapture- pass with Lean 4.32.0git diff --check- passa255608aae1abf31bea27d6a11d26e08d18f0b22Mathematical verification
Verifier and result: Pilot A's exact refutation and derived
disprovedstatus were independently audited in #41 / #42 / #43. This change binds witness2to that exact negation formalization and its protected receipt. The updated exact head passes the pinned real-Lean CI job. The new merged-tree package remains subject to the protected-publication download and independent audit required by #44 before that issue closes.Provenance and licensing
Provenance references: #41, #42, #43, #44; ADR-0009;
docs/trust/COUNTEREXAMPLE_REPAIR.md; protected publication receipt and retained closure.Risk and recovery
Known limitations: this does not prove the repaired claim, create pedagogy units, export release/RL data, or complete Pilot A / MathOS 1.0. A failed commit may leave only an unregistered content-addressed byte object, which is explicitly non-semantic.
Rollback or recovery plan: revert the merge. The change introduces no external dependency and no destructive data rewrite; the original claim and evidence are never mutated.
Follow-up work: independently audit the merged protected artifact, then open a separate slice to formalize and prove "Every prime number other than 2 is odd."
Review readiness