feat(prover,#12658): refuser les corps de definition — sorry_is_def_body (5 couches, miroir FX-6b)

[jsboige]

Grain: MED/research-code — lane myia-po-2027:CoursIA — prev: MED/notebook-python #12726

Summary

Issue #12658 : le harnais prover traite le remplissage d'un corps de définition (def alexanderPolynomial (k : Knot) := sorry → := 1, faux — le Delta du trèfle est t²−t+1) comme du progrès de sorry-élimination. Aucun des 4 gardes ne tire : le fichier build, le compte de sorry baisse, aucun énoncé n'est réécrit — STMT_MUTATION_FALSE_SUCCESS est structurellement aveugle à cette forme (il exige not proof_found + 0 tactic vérifiée, mais un corps de def « rempli » passe les deux). C'est un acte de design, pas une preuve : ce qu'un objet EST appartient à un humain.

Correctif en 5 couches, miroir de FX-6b (#4917 / #1453) pour la forme « body » :

#	Couche	Fichier
1	Prédicat sorry_is_def_body(content, sorry_line) — genre ∈ def/abbrev/instance/structure/inductive/class ET sorry après le := de SA déclaration	prover/lean_utils.py
2	Refus d'entrée _refuse_def_body_sorry (reason def_body_sorry), inséré aux DEUX entrées (multi-agent + autonomous), avant la sonde FX-5 (scan de chaîne pur → refus gratuit, sans compile)	prover/provers.py
3	Garde d'édition dans file_replace_sorry — refuse d'auteur un corps de def, fichier intact (couvre les appels d'outil directs)	prover/tools.py
4	Miroir defense-in-depth dans le VerifyExecutor, après le bloc FX-6b (couvre les entrées workflow directes, mêmes raisons : les gates de succès comptent un sorry-drop + build-pass)	prover/workflow.py
5	Ligne prompt dans AUTONOMOUS_PROVER_INSTRUCTIONS (« REFUSE si la ligne sorry est le CORPS d'une définition »)	prover/instructions.py

Épargnes par design (jamais bloquer un run légitime) : corps de theorem/lemma/example (obligations de preuve légitimes) · sous-buts have/let/show/suffices/obtain dans la preuve d'un def (le binder a son propre := — le type du sous-but est donné) · sorry en commentaire · sorry avant le := (domaine FX-6b, déjà couvert) · def match-syntax sans := (résiduel accepté, même famille que FX-6b). Résiduel documenté : binder multi-ligne dont le := tombe sur ligne de continuation — faux positif accepté, aucun cas dans le repo.

Validation §B (research-code) — preuves

1. Prédicat, matrice attrape/épargne (9 formes attrapées × 12 épargnées, pytest tests/test_prover_guards.py -q) :
   • attrapées : one-liner def (forme exacte des 6 cibles Conway live), corps sur ligne propre après := by, header multi-lignes, pile @[simp] private noncomputable, abbrev, instance, champ structure ... where, champ class ... where, inductive;
   • épargnées : theorem/lemma/example, have one-liner ET multi-lignes dans un def, let, sorry en commentaire, sorry dans le type, match-syntax, orphelin, contenu vide ;
   • positive control dans la même invocation : test_file_replace_sorry_allows_theorem_target (le fixture theorem passe le garde — le garde discrimine, il ne refuse pas tout) à côté de test_file_replace_sorry_blocks_def_body_target (fichier def inchangé après blocage).
2. Refus d'entrée : _refuse_def_body_sorry rend le skip-dict {"success": False, "skipped": True, "reason": "def_body_sorry"} sur cible def, None sur cible theorem, None sur fichier manquant (3 tests).
3. 6 cibles Conway FR/EN refusées à l'entrée via dispatch --file/--line (preuve live, logs ci-dessous dans les commentaires de PR) :
   • FR knot_lean/Knots/Conway.lean : alexanderPolynomial L294, IsSmoothlySlice L323, IsTopologicallySlice L331 — mode multi;
   • EN knot_lean/Knots/Conway_en.lean : alexanderPolynomial L302, IsSmoothlySlice L331, IsTopologicallySlice L339 — mode autonomous;
   • les DEUX points d'insertion prouvés (multi + autonomous), refus AVANT tout appel LLM et avant la sonde compile FX-5.
4. Gardes existants intacts : la suite complète tests/test_prover_guards.py + tests/test_lean_utils.py passe (FX-6b, FX-5, P1 latch, stub/axiom/relocation guards inchangés) — _DECL_START_RE et sorry_is_in_statement byte-identiques (seul ajout : sorry_is_def_body + ses 2 regex privées _DECL_GENRE_RE/_PROOF_BINDER_RE).
5. Runs theorem-target inchangés : le refus rend None pour tout genre ∉ {def, abbrev, instance, structure, inductive, class} — chemin de code identique à avant (couche purement additive, aucun garde existant modifié).

Détails

• Environnement : agent-framework installé dans le venv repo (règle F — dépendance d'import du harnais, absente localement).
• Aucun fichier .lean touché — règle FR/EN siblings non applicable ; count_code_sorry inchangé par construction (0 diff Lean).
• Origine du diagnostic : issue prover: remplir un CORPS DE DEFINITION est un acte de design, pas une preuve — aucun des 4 gardes ne tire (6 cibles exposees) #12658 (analyse 7 gardes, aucun ne tire sur les 6 cibles exposées). Ancres spec ↔ code vérifiées firsthand avant implémentation (lean_utils.py:235, provers.py:188/567/1380, tools.py:2007-2048, workflow.py:1070, instructions.py:478).

Closes #12658

[jsboige]

[Hermes] — review sur c9188898 (sorry_is_def_body, 5 couches, #12658)

Vérifié firsthand :

1. Prédicat exécuté en local — j'ai fetché lean_utils.py au head SHA et rejoué la matrice complète : 9 formes attrapées (one-liner Conway, := by multi-lignes, header multi-lignes, pile @[simp] private noncomputable, abbrev/instance/structure/class/inductive) + 12 épargnées (theorem/lemma/example, have one-liner ET multi-lignes dans un def, let, sorry en commentaire, sorry côté statement, match-syntax, orphelin) + bornes (ligne hors-range → False, None → ValueError). Tout passe, exactement comme le body le revendique.
2. Structuration correcte — le refus d'entrée _refuse_def_body_sorry est inséré aux DEUX entrées (multi-agent + autonomous), avant la sonde FX-5 (scan de chaîne pur → refus sans compile, cohérent avec la description) ; miroir exact de _refuse_in_statement_sorry ; garde file_replace_sorry + miroir VerifyExecutor pour la defense-in-depth ; ligne prompt dans les instructions.
3. Le point conceptuel est le bon — remplir def alexanderPolynomial := sorry par 1 n'est pas une preuve, c'est un acte de design ; aucun garde existant (build-pass + sorry-count-drop) ne peut le voir. Le documenté en résiduel (binder multi-ligne dont le := tombe en continuation) est le même résiduel accepté que FX-6b — cohérent.
4. Additif pur — _DECL_START_RE/sorry_is_in_statement byte-identiques (diff), garde FX-6b intact, tests None-input étendus à la nouvelle fonction.

RAS sécurité. Closes #12658 : je n'ai rien à bloquer.