New Challenge: Enrich MIR Consts

[dkcumming]

This PR proposes a new challenge to enrich the representation of MIR Consts extracted by verification tools.

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 write-up describing upstream compiler work to improve how MIR constants are represented/exposed to verification tools, focusing on preserving unevaluated forms and enriching public evaluated representations.

Changes:

• Introduces Challenge 31 specification (goal, motivation, approaches, success/correctness criteria).
• Documents current rustc/rustc_public constant representation gaps and relevant upstream code paths/issues.

[palinatolmach]

@feliperodri thanks for requesting the previous review! I've addressed the comments from Copilot so it's ready for another round, please let us know if there's anything we can do to assist the review process.

[feliperodri]

Really strong write-up @dkcumming! The concrete evidence (mir-json's post-eval decoder, KMIR's decoding.py, the upstream ty.rs:149 FIXME, project-stable-mir #96/#101) and the internal↔public type diagram make the problem and the design space very legible. Like its sibling #592, this fits area 1 of the effort (core verification mechanism), so I support adding it.

Two things I'd like before merge: (1) a SUMMARY.md entry — right now the challenge isn't linked into the book at all (general-rules.md requires it); and (2) an explicit acknowledgement that this is a non-standard infrastructure challenge taking the acceptance-criteria exception to the "automated, CI-checked solution" rule, since the deliverables are upstream rust-lang/rust PRs + written analysis. I've also suggested adding a repo-anchored non-regression criterion and clarifying the boundary with #592. Inline notes below.

[feliperodri]

This PR only adds the challenge file; there's no matching entry in doc/src/SUMMARY.md, so challenge 31 won't render in the book. general-rules.md lists "Add a link to the new challenge inside SUMMARY.md" as a required step for a new challenge. Could you add:

 - [31: Enriching MIR constants](./challenges/0031-enriching-mir-consts.md)

right after the challenge 30 line (or after 27 if #592 hasn't merged yet — mind the ordering so it lands after 30).

[feliperodri]

Same note I left on #592: general-rules.md says a reviewable solution "must be automated and should be checked and pass as part of the PR checks," and criteria A/B here resolve to upstream rust-lang/rust PRs plus a written analysis (with B explicitly allowing analysis to substitute for a merged change), none CI-checkable in this repo. That's fine, but only via the book's exception clause ("if it is specified as part of the acceptance criteria of the challenge being solved"). Could you add a sentence stating this challenge intentionally takes that exception? It makes the departure deliberate rather than something a future reviewer flags as a gap. (Criterion A's "an opt-in change is merged" is otherwise a nice objective anchor so thanks for that.)

[feliperodri]

Unlike #592, this challenge has no repo-anchored non-regression check, even though changing rustc's constant representation is exactly the kind of change that could perturb Kani. Consider adding a criterion analogous to #592's D: "At least one verification tool in this repo's CI (Kani, or KMIR once integrated) is rebuilt against a toolchain carrying the change, with all currently-resolved challenge proofs still passing." That gives one check anchored in this repository and guards existing verification results against regressions.

[feliperodri]

Good that you scope out broad rustc_public stabilisation here (that's #591/#592's territory). Since both challenges touch the internal↔public bridge and the public const surface, could you state the boundary between #594/#595 and #591/#592 explicitly... ideally in both tracking issues too? Mainly so a solver isn't blocked by a cross-dependency or credited twice for overlapping work (e.g. bridging ValTree on the public side shows up in both narratives).

[feliperodri]

Nit: this is a raw italicised URL; other challenges (and #592) use a markdown link, e.g. [#594](https://github.com/model-checking/verify-rust-std/issues/594). Also Line 3 **Status:** *Open* uses italic placeholder styling where others use plain Open. (let's remove Start/End dates since those fields are being dropped from the template.)

[feliperodri]

Optional/stylistic: the Goal runs ~30 lines and restates much of the Description (the monomorphisation "uroboros" detail). The template suggests a 1–2 sentence Goal. Trimming it to the two-gap summary and leaving the mechanism to Description would read a bit tighter. Not blocking.