Retire manual proof data CLI surfaces#1629
Merged
Merged
Conversation
WalkthroughThe PR removes the deprecated ChangesCLI Command Retirement: Proof and Witness Removal
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ 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 |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2d594e885d
ℹ️ 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".
Comment on lines
159
to
+160
| .arg("--formula") | ||
| .arg(&exhibit_formula) | ||
| .arg("formula.json") |
There was a problem hiding this comment.
Rejecting prove --formula is not safe yet because the checked-in Bug Zoo runner still invokes provekit prove --formula --json --quiet in menagerie/bug-zoo/src/lib.rs:1644-1648, and the build docs describe the Bug Zoo as a CI/tooling check. In any run with composition checks, this now exits at clap before producing the JSON verdict the runner parses, so the Bug Zoo experiments fail rather than reporting red/green obligations; migrate that runner to a supported gate or keep a compatible path until it is updated.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
implementations/rust/provekit-cli/src/cmd_prove.rs (2)
481-489:⚠️ Potential issue | 🟠 Major | ⚡ Quick winReject conflicting
provemodes instead of picking one silently.
run()gives--artifact/--proof/--policyprecedence over--kit, and the kit path also ignores verifier-only knobs like--withand the empirical-witness flags. For example,prove --kit rust --proof receipt.jsonruns admission verification, not the conformance gate.Suggested fix
pub fn run(args: ProveArgs) -> u8 { + if args.kit.is_some() + && (args.artifact.is_some() + || args.proof.is_some() + || args.policy.is_some() + || !args.with.is_empty() + || args.require_empirically_witnessed.is_some() + || args.require_fixture.is_some() + || args.consensus_policy.is_some()) + { + eprintln!( + "{}: --kit cannot be combined with prove/admission flags", + "error".red().bold() + ); + return crate::EXIT_USER_ERROR; + } + if args.artifact.is_some() || args.proof.is_some() || args.policy.is_some() { return run_admission_gate(&args); }🤖 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 `@implementations/rust/provekit-cli/src/cmd_prove.rs` around lines 481 - 489, The run function currently prefers admission mode (run_admission_gate) when any of args.artifact/args.proof/args.policy are set and silently ignores args.kit and verifier-only knobs; change it to detect conflicting modes and reject the invocation with a clear error instead of picking one: in run(ProveArgs) check for mutually exclusive combinations (if args.kit.is_some() && (args.artifact.is_some() || args.proof.is_some() || args.policy.is_some() || args.with.is_some() || args.empirical_witness_flags_are_set())) and return a non-zero error/print a message explaining the conflict (e.g., request user to choose either kit/conformance via run_kit or artifact/proof/policy admission via run_admission_gate), preventing run_admission_gate or run_kit from being called when both modes are present; update any calling code/tests that expect the old precedence accordingly.
186-264:⚠️ Potential issue | 🟠 Major | ⚡ Quick winKeep
--jsonoutput machine-readable.
capture_rpc()still writesdispatch:/ok:banners to stdout wheneverquietis false, soprovekit prove --kit <kit> --jsonemits non-JSON bytes before the JSON report.Suggested fix
-fn capture_rpc( - project_root: &std::path::Path, - surface: &str, - quiet: bool, -) -> Result<CapturedRpc, String> { +fn capture_rpc( + project_root: &std::path::Path, + surface: &str, + quiet: bool, + json_out: bool, +) -> Result<CapturedRpc, String> { let manifest = find_manifest(project_root, surface)?; - if !quiet { + if !quiet && !json_out { println!( "{}: surface=`{}` plugin=`{}` command={:?}", "dispatch".green().bold(), @@ - if !quiet { + if !quiet && !json_out { if let Some(name) = init_response .get("result") .and_then(|r| r.get("name")) @@ - let rpc = match capture_rpc(&project_root, &surface, quiet) { + let rpc = match capture_rpc(&project_root, &surface, quiet, json_out) {Also applies to: 385-427
🤖 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 `@implementations/rust/provekit-cli/src/cmd_prove.rs` around lines 186 - 264, The function capture_rpc prints human-readable banners to stdout (e.g., the println! with "dispatch" and the "ok" message) which corrupts machine-readable --json output; change those prints to write to stderr instead (use eprintln! or write to std::io::stderr()) when quiet is false or when JSON output is requested so stdout remains pure JSON. Update the println! calls in capture_rpc (the dispatch banner that uses manifest.name/manifest.command and the plugin-ready "ok" message) and make the equivalent change in the other similar block around the later region (lines ~385-427) so all human banners go to stderr, not stdout.
🤖 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.
Outside diff comments:
In `@implementations/rust/provekit-cli/src/cmd_prove.rs`:
- Around line 481-489: The run function currently prefers admission mode
(run_admission_gate) when any of args.artifact/args.proof/args.policy are set
and silently ignores args.kit and verifier-only knobs; change it to detect
conflicting modes and reject the invocation with a clear error instead of
picking one: in run(ProveArgs) check for mutually exclusive combinations (if
args.kit.is_some() && (args.artifact.is_some() || args.proof.is_some() ||
args.policy.is_some() || args.with.is_some() ||
args.empirical_witness_flags_are_set())) and return a non-zero error/print a
message explaining the conflict (e.g., request user to choose either
kit/conformance via run_kit or artifact/proof/policy admission via
run_admission_gate), preventing run_admission_gate or run_kit from being called
when both modes are present; update any calling code/tests that expect the old
precedence accordingly.
- Around line 186-264: The function capture_rpc prints human-readable banners to
stdout (e.g., the println! with "dispatch" and the "ok" message) which corrupts
machine-readable --json output; change those prints to write to stderr instead
(use eprintln! or write to std::io::stderr()) when quiet is false or when JSON
output is requested so stdout remains pure JSON. Update the println! calls in
capture_rpc (the dispatch banner that uses manifest.name/manifest.command and
the plugin-ready "ok" message) and make the equivalent change in the other
similar block around the later region (lines ~385-427) so all human banners go
to stderr, not stdout.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 94dc32bb-c744-453c-a9f0-05f894facc68
📒 Files selected for processing (28)
README.mddocs/audits/2026-05-18-kit-as-substrate-participant-vision.mddocs/contributing/build.mddocs/explanation/use-cases.mddocs/how-to/debugging-a-failed-handshake.mddocs/papers/03-substrate-not-blockchain.mddocs/reference/per-language-status.mddocs/reference/protocol-extensions.mddocs/superpowers/plans/2026-05-08-bridgeworks-white-room-contract-stack.mddocs/superpowers/specs/2026-05-08-bridgeworks-white-room-contract-stack-design.mdimplementations/rust/provekit-cli/src/cmd_proof.rsimplementations/rust/provekit-cli/src/cmd_prove.rsimplementations/rust/provekit-cli/src/cmd_witness.rsimplementations/rust/provekit-cli/src/main.rsimplementations/rust/provekit-cli/tests/cli_surface.rsimplementations/rust/provekit-cli/tests/cmd_emit_go_testify.rsimplementations/rust/provekit-cli/tests/cmd_emit_go_testing.rsimplementations/rust/provekit-cli/tests/cmd_emit_java_junit.rsimplementations/rust/provekit-cli/tests/cmd_emit_python_pytest.rsimplementations/rust/provekit-cli/tests/cmd_emit_scala_scalatest.rsimplementations/rust/provekit-cli/tests/cmd_emit_swift_xctest.rsimplementations/rust/provekit-cli/tests/cmd_emit_typescript_vitest.rsimplementations/rust/provekit-cli/tests/fixtures/checked_contradiction.jsonimplementations/rust/provekit-cli/tests/lower_formula.rsimplementations/rust/provekit-cli/tests/proof_check.rsprotocol/conformance/proof-protocol/README.mdprotocol/specs/2026-05-02-binary-attestation-protocol.mdprotocol/specs/2026-05-14-witness-consensus-promotion.md
💤 Files with no reviewable changes (6)
- implementations/rust/provekit-cli/tests/fixtures/checked_contradiction.json
- implementations/rust/provekit-cli/tests/lower_formula.rs
- implementations/rust/provekit-cli/src/cmd_proof.rs
- implementations/rust/provekit-cli/src/cmd_witness.rs
- docs/reference/protocol-extensions.md
- implementations/rust/provekit-cli/tests/proof_check.rs
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
1 participant
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.
Summary
prove(--formula,--target,--output)proofandwitnessprovekit dumpas the supported .proof diagnostic surfaceprovekit proof/ publicwitnesscommand referencesVerification
cargo test -p provekit-cli --test cli_surface --manifest-path implementations/rust/Cargo.toml -- --nocapturecargo test -p provekit-cli --manifest-path implementations/rust/Cargo.toml --test cmd_emit_go_testing --test cmd_emit_go_testify --test cmd_emit_python_pytest --test cmd_emit_java_junit --test cmd_emit_typescript_vitest --test cmd_emit_swift_xctest --test cmd_emit_scala_scalatest -- --nocapturecargo test -p provekit-cli --manifest-path implementations/rust/Cargo.toml --tests --no-runcargo fmt --manifest-path implementations/rust/provekit-cli/Cargo.toml --checkgit diff --checkNote: TypeScript/Vitest emit integration retained the existing local dependency skip when TS emitter deps are not built.
Summary by CodeRabbit
Removed Features
provekit proofcommand and all its subcommandsprovekit witnesscommandprovekit proveNew Features
provekit proveandprovekit verifycommandsDocumentation