feat: restrict edits to the proof body (lock challenge-file imports/opens)

[KrystianNowakowski]

What

Adds an opt-in restrict_to_proof_body flag on ProverConfig (default false). When enabled, the prover only edits the proof body of the target theorem — it never writes new import or file-level open statements into the file. This satisfies the AI4Math / Codabench TCS competition rules:

1. Only fill in the sorry placeholders … do not modify any other part of those files.
2. Do not change the import statements in the challenge files.

Default-off, so ax-prover's general behavior (where adding imports is legitimate) is unchanged.

How

• Config: restrict_to_proof_body: bool = False on ProverConfig.
• Enforcement: TemporaryProposal skips edit_imports/edit_opens when the flag is set — the proof body (edit_function) is still applied. Wired at both the builder node and the reviewer's apply_permanently path, so the final committed file is clean too.
• Feedback: when the proposer still emits imports/opens under a locked file, a warning is prepended to the build-failure error_output (no messages.py changes — keeps this independent of the lemma-stripping branch).
• Prompt: a PROOF_BODY_RESTRICTION_PROMPT fragment is appended via a new, testable build_proposer_system_prompt() helper when the flag is on (covers both iterative and single-shot prompts).

Tests

253 unit tests pass; ruff clean. Includes a regression guard asserting _proposer_node actually calls the prompt builder (helper-only tests can pass while the wiring is broken).

Notes

• Activation (restrict_to_proof_body: true) is applied to the experiment profile (opus48_local.yaml) on the experiment branch after merge — out of scope here.
• Out of scope (per spec): auxiliary files (Rule 4), axiom checking (Rule 5).
• Design spec: docs/superpowers/specs/2026-06-05-restrict-edits-to-proof-body-design.md

🤖 Generated with Claude Code

---

Note

Medium Risk
Changes how proposals are applied to disk on build and final approval when the flag is on; default-off limits blast radius, but mis-enabled config could hide missing imports until compile failures.

Overview
Adds opt-in restrict_to_proof_body on ProverConfig (default false) so challenge-style runs only change the target theorem’s proof body, not new file-level import / open lines.

When enabled, TemporaryProposal skips applying proposed imports/opens (proof code still applies) at both the builder temp-build path and reviewer apply_permanently. The proposer gets a locked-file prompt via build_proposer_system_prompt() / PROOF_BODY_RESTRICTION_PROMPT, and _dropped_preamble_warning is prepended to failed-build feedback and passed into SorriesGoalStateFeedback on successful builds that still have sorries. Unit tests cover config defaults, temp-file behavior, prompt assembly, and wiring guards in _proposer_node / _builder_node. Design/plan docs are added under docs/superpowers/.

^{Reviewed by Cursor Bugbot for commit 01cc7c9. Bugbot is set up for automated code reviews on this repo. Configure here.}

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 3c916b2. Configure here.}

[cursor]

Timeout path omits preamble warning

Medium Severity

With restrict_to_proof_body enabled, dropped-import/open feedback is prepended only when Lean returns a normal compilation failure. A LeanBuildTimeout still emits plain BuildFailedFeedback text, so the proposer never sees the IMPORTS/OPENS IGNORED warning on that path.

 

^{Reviewed by Cursor Bugbot for commit 3c916b2. Configure here.}