New challenge: Progress Public MIR

[dkcumming]

#595

This PR proposes a new challenge to progress Public MIR's API stability.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds a new “Challenge 30” document describing a time-boxed effort to improve Public MIR (rustc_public) API stability/usability for verification tooling, and links it from the doc summary.

Changes:

• Added a new challenge write-up: “Progressing Public MIR for verification tool infrastructure”.
• Documented motivation, scope, success criteria, and correctness criteria for upstreaming missing rustc_public coverage.
• Updated the documentation summary to include challenges 28–30.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 7 comments.

File	Description
doc/src/challenges/0030-progress-public-mir.md	New challenge document detailing goals/scope/criteria for improving Public MIR for verification tools.
doc/src/SUMMARY.md	Adds navigation entries for challenges 28–30, including the new challenge 30.

[palinatolmach]

@feliperodri similarly to #595, I've addressed the previous comments, so this PR is ready for another review. Please let us know if there's anything we can do to assist the review process.

[feliperodri]

@palinatolmach Thanks for this! The topic is squarely in scope. The book classifies the effort into three areas, and this fits area 1 ("contributing to the core mechanism of verifying the Rust standard library"). Progressing rustc_public so tools stop round-tripping through rustc_internal is a real, well-motivated source of fragility for Kani/KMIR, and the write-up is unusually clear and honest about the risks.

My hesitation is entirely about verifiability, since this challenge's deliverables live upstream in rust-lang/rust and in workgroup discussion rather than in Kani harnesses that pass in this repo's CI. I've left inline notes on the success criteria. Net: I support adding it, provided we (a) explicitly acknowledge it as a non-standard infrastructure challenge that takes the acceptance-criteria exception to the "automated, CI-checked solution" requirement, and (b) add at least one objective floor so "resolved" is adjudicable. The rest are minor.

[feliperodri]

The general-rules.md Solution Requirements state a solution is only reviewed if it "must be automated and should be checked and pass as part of the PR checks." Criteria A–C here are inherently subjective/best-effort ("convert as many … as is feasible", "a blocker presented with analysis counts toward the criterion") and can't be evaluated by CI, only D is CI-anchored. That's not disqualifying: the book allows exceptions "if it is specified as part of the acceptance criteria of the challenge being solved." Could we add an explicit sentence here stating this challenge intentionally takes that exception (infrastructure challenge, deliverables are upstream PRs + design analysis, not repo-local proofs)? That makes the departure deliberate rather than an oversight a future reviewer trips over.

[feliperodri]

Because A–C are best-effort, two committee members could reasonably disagree on whether a submission "resolved" the challenge and this will eventually carry a reward. Consider adding a minimal concrete floor here, e.g. "at least N of the named consumer shims (e.g., Kani internal_mir.rs, stable-mir-json) are either removed via a merged upstream PR or catalogued with a taxonomy under criterion C." An objective anchor keeps adjudication (and the reward decision) tractable without removing the flexibility the rest of the criterion needs.

[feliperodri]

Worth making explicit that completion depends on the project-stable-mir](https://github.com/rust-lang/project-stable-mir) workgroup reaching consensus... something the solver doesn't control, and which the Motivation itself notes "has historically blocked some conversions." I think the criterion-A/C "taxonomy counts as a deliverable" escape hatch is the right mitigation; I'd just call it out here so a solver understands upfront that blocked-but-well-analysed work is an accepted outcome, and so the reward committee is comfortable rewarding design/analysis output rather than only merged code.

[feliperodri]

Blocker: CI with any verification tool that has been integrated into the contest can be broken. You can bypass a tool if your approach is design to specific tools, but it cannot broke any tool in CI.

[feliperodri]

Nit: other challenge files use a plain Open here; the italics/asterisks are leftover template placeholder styling. (Also, Start/End dates... don't worry about the TBDs; we're planning to drop those fields from the template entirely, so you can remove them completley as well.)

[feliperodri]

Thank you!!!