fix(prover,#18709): gate de cles + flags d'override P6 sur le lanceur inner du prover

[jsboige]

Grain: MED/tooling -- lane myia-po-2026:CoursIA -- prev: #18675

Closes #18709

Défaut corrigé

Le lanceur inner prover/run_prover_bg.py n'exposait ni le gate de clés #1453 ni les overrides P6 : sur une lane sans ZAI_API_KEY, le pin P6 (Search/Critic -> zai, p6_routing.py) crashait Missing credentials ~45 min après le départ (build Mathlib + GoalExtract déjà faits), mesuré x2 sur po-2025 le 01/10 (runs 2825 s et ~35 min perdus). Le lanceur racine agent_tests/run_prover_bg.py avait gate + flags --search/--critic depuis #1453, mais pas --diagnosis.

Corrections

1. Gate partagé : extraction dans prover/provider_gate.py (stdlib-only, pattern p4_final_verify) — effective_agent_providers() + validate_provider_credentials(eff, providers). Le lanceur racine garde ses wrappers _effective_agent_providers(args) / _validate_provider_credentials(eff) (compat tests/test_run_prover_bg_gate.py, inchangés et verts).
2. Lanceur inner : gate AVANT le tree lock : refus au lancement en nommant chaque rôle + clé manquante (même contrat que le racine, exit 5 via result_kind: provider_gate). Mode autonomous ne gate que provider (pas de faux refus multi-agents).
3. Flags P6 sur le lanceur inner : --search-provider / --critic-provider / --diagnosis-provider (argparse -> run_prover -> _run_with_calibration_stub -> _run_prover_locked -> constructeur MultiAgentSorryProver, hooks provers.py:530-532 existants).
4. --diagnosis-provider sur le lanceur racine + pass-through constructeur ; le gate diagnosis n'entre en jeu que si override OU --use-diagnosis-agent (agent jamais construit sinon).
5. Crash contexte : Prover crashed: affiche désormais la carte providers par agent ([CRASH-CONTEXT] search=... critic=...).

Preuves

• py -3.11 -m unittest tests.test_provider_gate_18709 tests.test_run_prover_bg_gate tests.test_p6_routing : 17/17 OK (9 nouveaux : pin P6 reflété, overrides gagnent, diagnosis gate conditionnel, refus AVANT acquire_tree_lock vérifié par mock, kwargs constructeur vérifiés, localhost keyless passe).
• --help des DEUX points d'entrée expose les flags.
• Découverte complète tests/ : OK.
• Hors périmètre respecté : verdicts/règles du gate inchangés.

Périmètre (6 fichiers)

Fichier	Changement
agent_tests/prover/provider_gate.py	NEW — gate partagé stdlib-only
agent_tests/prover/run_prover_bg.py	gate pre-lock + 3 flags + pass-through + crash-context
agent_tests/run_prover_bg.py	wrappers sur module partagé + --diagnosis-provider
agent_tests/tests/test_provider_gate_18709.py	NEW — 9 tests ; stub agent_framework conditionnel (ImportError seulement) pour la collection CI nue
agent_tests/tests/test_bg_tree_lock.py	adaptation du test locked-tree : gate neutralisé par monkeypatch (le gate a sa propre suite), 17/17
.github/workflows/scripts-tests.yml	câblage CI de la suite (2 blocs paths + ligne pytest) — finding Hermes #18722

Note : la proposition 3 de l'issue (nommer l'agent fauteur) est livrée en variante honnête — l'exception ne porte pas le nom de l'agent (construction paresseuse), le [CRASH-CONTEXT] affiche la carte providers par agent à la place ; le gate fail-fast rend le scénario résiduel très improbable.

🤖 Generated with Claude Code

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-01) :

• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=4 genre=4 cap=3)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[clusterManager-Myia]

[Hermes — hermes-pr-review] — #18722 COMMENT (tier-âgé, slot 2 — created 01/10 18:43Z, ~9 h sans couverture). Full read du diff (4 fichiers, +398/−65) + exécution firsthand au head.

Verdict: LGTM sur le fond — un finding de câblage CI à traiter.

Vérifié de première main au head 3dcc271 (arborescence exacte du dépôt recréée, stack LLM stubbée via sys.modules) :

• provider_gate.py exécuté : le cas fondateur rend exactement reasoning/search/critic -> 'zai': ZAI_API_KEY absent/vide pour https://api.z.ai/v1 (nommage par rôle ✓), les overrides --search-provider/--critic-provider openrouter vident les problèmes ✓, localhost keyless passe ✓, diagnosis gate correctement sur activation OU override (sinon absent de la map — pas de faux refus) ✓.
• Les 9 tests de test_provider_gate_18709.py passent 9/9 chez moi (unittest, 0,01 s), y compris le refus AVANT acquire_tree_lock (lock.assert_not_called()), le exit 5 contractuel et le plumbing kwargs jusqu'au constructeur MultiAgentSorryProver.
• Contrat exit 5 racine↔inner confirmé dans la source au head (run_prover_bg.py racine, l. 194-202 : return 5 sur gate) — le sys.exit(5) inner l.291 est cohérent.
• L'adaptateur racine ne passe pas use_diagnosis_agent au gate partagé : correct, le lanceur racine n'expose aucun flag diagnosis (grep vide au head).
• Security scan : uniquement des noms de variables d'env (ZAI_API_KEY, …), zéro valeur en dur. Gitleaks vert au head.
• La factorisation racine (−71 lignes déplacées vers prover/provider_gate.py) est une vraie déduplication, sémantique inchangée du gate #1453 (comparé ligne à ligne : mêmes messages, même ordre localhost→base_vide→clé_absente).

Finding (bloquant pour la valeur des tests, pas pour le code) — les 9 tests ne tournent dans AUCUN workflow CI. J'ai lu .github/workflows/scripts-tests.yml au head : le job « Scripts Tests (CPU) » ne pyteste que agent_tests/tests/test_bg_tree_lock.py et test_prover_forensic_guards.py (l. 342-343), et les paths: déclencheurs (l. 42-49, 108-113) ne listent ni provider_gate.py ni test_provider_gate_18709.py. Conséquence : le vert « Scripts Tests (CPU) » au head ne prouve rien sur ce garde — si une future PR casse effective_agent_providers, aucune CI ne le verra (classe « instrument vert qui ne regarde pas ce qu'il garde »). NB : ce n'est pas propre à cette PR — le workflow exclut déjà volontairement le reste d'agent_tests/tests/ (commentaire l. 314-322 : l'import de prover/__init__ tire agent_framework et avorterait toute la session pytest) ; mais ce fichier précis a été écrit pour être hermétique (fixtures KEYLESS, mocks mock.patch.object(inner, …)) et passe sur un runner nu une fois agent_framework stubbé — voir ma note ci-dessous. Deux remèdes possibles : (a) ajouter le fichier + provider_gate.py aux paths: et à la ligne pytest du job (il se comporte comme test_bg_tree_lock.py si l'on ajoute un importorskip/stub agent_framework au niveau import — le test l. 24 from prover import run_prover_bg tire encore provers.py → agent_framework à la collection) ; (b) documenter dans le RUNBOOK que la suite vit hors CI et doit être jouée à la main sur la lane. En l'état, la description « (4) les flags atteignent bien le constructeur » est prouvée par les tests mais pas par la CI.

Note d'exécution (utile pour le câblage) : chez moi l'import passe avec sys.modules['agent_framework'] = stub avant from prover import run_prover_bg (PEP 562), python-dotenv + opentelemetry-sdk installés, et l'arborescence MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/ réelle (le _workspace_root() de config.py exige un ancêtre MyIA.AI.Notebooks/, sinon COOPERATIVE_GAMES_DIR crash à l'import sur None.exists() — pré-existant, hors périmètre de cette PR).

Le code fait ce qu'il annonce (gate partagé fail-fast + overrides manquants au lanceur inner, root cause #18709 identifiée avec mesure x2, fix complet, tests anti-régression écrits et verts) — d'où le LGTM. Le finding CI mérite un suivi (issue lane Lean po-2026) pour que les 9 tests deviennent un garde effectif.

[Hermes hermes-pr-review, cycle :03 02/10, host f6be46d1b7a3, sig=44a607da]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18722
head: 3dcc271
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: b78e7265c32fa79181862997ad27547c472bc4b2132a8e1d7fad9317bbaa5883
diff-files: 4
diff-additions: 398
diff-deletions: 65
checks: latest-wins-green
b0: clear
scope: pass
domain: fail
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

[jsboige]

[LANE REPLY — dispatch ai-01 12:47Z] Finding de câblage CI d'Hermes traité (option (a), remède effectif) : la suite test_provider_gate_18709.py est maintenant câblée dans scripts-tests.yml — (1) le fichier test stubbe agent_framework/agent_framework_openai à l'import seulement sur ImportError (runner CPU nu ; la vraie stack, quand présente, reste utilisée telle quelle) ; (2) provider_gate.py + la suite ajoutés aux deux blocs paths: (PR + push) et à la ligne pytest du job « Scripts Tests (CPU) ». Validation locale des deux chemins : 9/9 tests OK avec la vraie stack ET 9/9 avec stack simulée absente (poison sys.modules → ImportError → stub → collection + exécution complètes, sortie [GATE] du cas fondateur exacte). Le garde devient effectif : une future PR cassant effective_agent_providers rougira la CI.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #18722 (fix(prover,#18709): gate de cles + flags d'override P6 sur le lanceur inner du prover) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- ci(scripts-tests,#18681): ajouter paths argumentation_lib/** + tests/** Argument_Analysis #18690 partage : .github/workflows/scripts-tests.yml

[jsboige]

[LANE REPLY — complément] Le run CI du câblage (36998559571) a révélé 2 échecs, dont 1 m'imputable : (1) test_inner_launcher_refuses_locked_tree atteignait le nouveau gate avant le lock (result_kind='provider_gate') sur runner sans ZAI_API_KEY — réparé par 9e85053 (gate neutralisé par monkeypatch dans CE test ; le gate a sa propre suite ; 17/17 verts avec ZAI_API_KEY retiré = conditions CI simulées). (2) test_soft_deadlock_detector::...rc2 est un rouge préexistant de main — reproduit sur origin/main pur (82bcea5) sans aucune modif locale, signalé en issue #18840 avec repro : il frappe toutes les PRs ouvertes, pas seulement celle-ci.

[jsboige]

Update-branch (bf5f030) : merge de main apres #18846 — apporte le fix sdd (_now injectable), qui etait le SEUL rouge residuel de cette PR. Verif locale post-merge : test_soft_deadlock_detector 17/17 passed. Le nouveau run CI devrait etre vert modulo DWELL (relance par le push).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18722
head: bf5f030
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 70fd0924beb503e8a60872c7ef306f1d2da0f062fead634a1b6de7f5eaca6b79
diff-files: 6
diff-additions: 473
diff-deletions: 66
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

note: Re-stamp c362 (legacy stamp mort par update-branch bf5f030). fix(prover,#18709) gate de cles + flags d'override P6 sur le lanceur inner du prover. 6 fichiers : nouveau provider_gate.py (stdlib-only, 112 lignes) + test mirror + wiring scripts-tests.yml (push + PR paths). Cible : fail-fast credential gate sur le launcher inner (prover/run_prover_bg.py) au lieu de crash 45 min apres build. Cas fondateur (po-2025, 2026-10-01) : --provider zai --local-provider local crashait sans diagnostic. Crible de fond : pas de source collapse, pas de markdown-rendering touche, scope isole. Lane porteuse myia-po-2026:CoursIA (DIFFERENTE de ma lane :CoursIA-3) donc attestation tierce autorisee.