feat(lean,#15666): T5a validation charge bornée — harnais de sondes pendant un build lake réel sous lean_exec

[jsboige]

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

Le livrable

scripts/lean/validate_bounded_load.py — T5a de l'EPIC #15666 : le harnais qui valide l'organe lean_exec (T1-T3, sur main) sur charge réelle. L'incident fondateur (~30 lean.exe à ~95 % CPU → DriveFS tombe → Claudish → reboot) n'est contredit par aucune preuve tant que personne n'a mesuré la machine pendant une vraie compilation confinée. Ce harnais est cette preuve, réutilisable.

Ce qu'il mesure PENDANT la compilation

Critère dur	Mesure	Régime de l'incident
population_cap	population native lean/lake échantillonnée avec la même fonction de mesure que l'organe (lean_exec.scan_native_population, importé — pas une seconde opinion qui dériverait) ; max observé ≤ cap	30 lean sous cap 8
drivefs_alive	listdir chronométré sur le lecteur monté (G:\Mon Drive), sous garde-fou temps — un timeout de sonde = ECHEC	DriveFS mort = premier symptôme mesuré de l'asphyxie
spawn_p95	latence pour spawner un python trivial + attendre sa mort — proxy de la santé ordonnanceur ; p95 charge ≤ max(5× p95 baseline, plancher 5 s)	l'ordonnanceur meurt en premier
organ_postcondition	last_run.json de l'organe : status ok, orphelins vides — lu et réconcilié avec la commande attendue et un run_id frais (un enregistrement d'un autre run — cmd différente, ou crash avant émission laissant le run précédent, même commande — est rejeté, pas validé)	—

RAM libre rapportée sans seuil inventé (l'organe plafonne déjà le run via Job Object). Chaque critère PASS/FAIL cite sa mesure (chiffres dans le détail), jamais un aveu nu.

Génération de la charge — réelle, pas fictive

--touch N augmente le mtime des N modules propres les plus anciens du lake (contenu strictement inchangé → arbre git propre ; modules sous .lake/ et lakefile.lean exclus) — la cascade de recompilation qui suit est la charge. Le harnais lance lean_exec.py run -- lake build dans le lake fourni : c'est le chemin exact d'un futur appelant migré.

La mesure réelle (siège po-2026, lake 5.0.0 / toolchain 4.31.0-rc1, cache Mathlib 8345 oleans)

Run 1 — le scénario incident, arrêté net (budget défaut 2) : --touch 10 sur game_theory_lean (47 modules propres, cascade StableMarriage + GameTheory.lean), lake build -Kjobs=5 sous l'organe. La supervision budget de l'organe tire à 96,8 s : budget_violation: "4 lean/lake descendants > budget 2", status timeout, exit 124, arbre tué, orphelins = 0. Pendant le kill et la charge (population max observée 7 ≤ cap 8, 31 échantillons) : DriveFS jamais en timeout (p95 234 ms), spawn p95 78 ms (baseline 47 ms), RAM libre min 28,3 Go. La machine est restée vivable pendant exactement le régime qui l'avait tuée en septembre — et le harnais le prouve chiffres en main, pas par affirmation.

Run 2 — 15 minutes de charge soutenue (budget 8) : la cascade de 10 modules ne tient pas sous le plafond — l'organe tire au mur 900 s (duration 904 s, status timeout, exit 124), orphelins = 0. Pendant ces 15 min de charge continue (population max 7 ≤ cap 8, 253 échantillons) : DriveFS jamais en timeout (p95 203 ms), spawn p95 79 ms contre 78 ms de baseline — indiscernable de l'inactif —, RAM libre min 26,9 Go. La preuve de sûreté vaut ici plus qu'un succès rapide : c'est un quart d'heure du régime exact de l'incident, sans qu'aucune sonde ne bronche, et un kill d'arbre propre à la fin.

Run 3 — queue résiduelle, 30 min de charge (plafond 1800 s) : le run 2 a touché CooperativeGames/Basic.lean, module racine — la cascade aval est le lake entier (47 modules + jumeaux _en). 30 minutes de compilation n'ont pas suffi : l'organe tire au mur 1800 s (duration 1805 s), orphelins = 0, et sur 414 échantillons de cette demi-heure de charge continue : population max 7 ≤ 8, DriveFS jamais en timeout (p95 47 ms), spawn p95 78 ms, RAM min 27,8 Go. Le kill au mur n'est pas un défaut de l'organe ni du harnais — c'est un plafond assume contre un build sous-dimensionne ; la leçon opérationnelle (dimensionner --timeout a la cascade visee) va dans les limites ci-dessous.

Run 4 — le build mène à terme (lake borné, budget 8) : social_choice_lean (sources via srcDir partagé, oleans en retard → lake build avait du travail réel en attente ; touched: [] est correct, aucun module propre dans le répertoire). PASS 4/4 : organe status=ok, enfant exit 0, duration 150 s, orphelins = 0, population max 2 ≤ cap 8 (45 échantillons), DriveFS jamais en timeout (p95 125 ms), spawn p95 78 ms, RAM min 28,1 Go. La voie-success du harnais (verdict PASS sur un vrai build) est exercée, pas seulement la voie-échec.

Constat opérationnel pour T5b (consigné mémoire lane) : les défauts de l'organe sont internement incohérents pour un lake build nu — jobs = cpu//4 = 5 fait spawner ~7 lean/lake, budget défaut = 2 les tue à ~100 s. Tout appelant migré devra passer --budget >= jobs+1. Ce n'est pas un bug du kill (il est propre, orphelins 0) ; c'est une contrainte à documenter au moment de la migration.

Pourquoi T5a seul (le scoping, mesuré sur le source)

La moitié « migration » de T5 (T5b) exige des extensions de l'organe : run_command sur origin/main n'a ni cwd, ni input, ni capture de sortie — or lean_rlvr_verifier._run_lean (MyIA.AI.Notebooks/GenAI/PostTraining/verifiers/lean_rlvr_verifier.py:185) a besoin des trois (cwd=project_dir, input=source, capture_output=True), et po2026_recover_build.py:156,178 de cwd + env PATH sanitizé. Migrer sans ça = soit empiler sur l'organe, soit maquiller en os.chdir (thread-unsafe). De plus l'allowlist T4 (PR #16196, OPEN) n'est pas mergée. T5b reste résiduel, documenté au claim (c.5679738618).

Tests — scripts/tests/test_validate_bounded_load.py (21 contrats)

1-2. verdict propre : 4 critères cités avec leurs chiffres ; p95 sur listes connues
3-7. le régime de l'incident échoue : population 12 > cap 8 ; sonde DriveFS timeout ; spawn p95 40 s ; organe refused ; organe orphelins
8. spawn dégradé mais SOUS le plancher (baseline lente 2 s → borne 10 s, charge 8 s) = PASS : la borne est relative à la machine, pas un absolu inventé
9-11. pas de faux pass : sonde DriveFS indisponible = note honnête, pas un succès ; 0 échantillon de charge = non vérifiable ; enregistrement organ absent ne valide rien
12-14. le harnais ne se bloque pas : sonde abandonnée au timeout rend la main (< 3 s) ; l'échantillonneur s'arrête à la mort de la charge et rend la main APRÈS ; mur du harnais signalé
15-17. --touch exclut .lake/ et lakefile.lean, bump exactement N mtimes, contenu inchangé ; CLI exige un lakefile ; read_organ_record rejette le stale (cmd différente)
18-21. les faux-pass de la review exact-head sont fermés : population non mesurable (run tout -1) échoue le critère avec « 0 mesure de population valide » ; population mixte jugée sur les seules mesures valides, les deux comptes cités ; read_organ_record rejette le stale même commande (run_id préexistant = crash avant émission, et format sans run_id) ; known_run_ids lit aussi le registre des runs vivants

Aucun lake ni lean requis pour les tests : le verdict est une fonction pure sur échantillons fabriqués, l'échantillonneur se teste sur un enfant python.

Deux défauts attrapés par le développement lui-même : un stdout=PIPE non drainé pendant l'échantillonnage (deadlock garanti — le build lake emplit bien plus que le buffer ; sortie redirigée vers fichier), et nargs="+" d'argparse qui s'arrête au premier token -- de la commande (--cmd lake --version devenait --cmd lake + flag inconnu → REMAINDER, même sémantique que l'organe).

Validation

• pytest scripts/tests/test_validate_bounded_load.py → 21 passed in 1.90 s (17 contrats + 4 nouveaux contrats faux-pass)
• Suite complète post-base : python -m pytest scripts/tests/ → 5665 passed, 30 skipped, 5 xfailed in 775.90 s (origin/main 5a1989a92 intégré, merge commit f5106afcc)
• Smoke CLI end-to-end (commande triviale lake --version sous l'organe) → PASS 4/4, rc=0 ; et la version où l'organe échoue honnêtement (child_failed) → FAIL nommé, rc=1
• Runs réels sous charge (4, détail ci-dessus) : kills de sécurité prouvés (budget à 96,8 s ; murs à 904 s et 1805 s) avec 0 orphelin chacun, 712 échantillons cumulés de charge 2-7 lean/lake, DriveFS jamais en timeout, spawn p95 ≤ 79 ms sur tous les runs ; et une passe complète PASS 4/4 (run 4, build mené à terme).

Limites honnêtes

• La sonde DriveFS dépend du lecteur monté sur le siège (G:\Mon Drive par défaut) : absente → sonde unavailable notée, le critère timeout n'est pas vérifiable sur ce siège (pas un faux pass).
• Le spawn p95 borne un proxy de santé système, pas la latence de Claudish lui-même (aucun endpoint de santé stable à sonder depuis un script ; l'ordonnanceur est ce qui meurt en premier dans l'incident mesuré).
• Le seuil population ≤ cap vérifie le plafond de l'organe, pas pourquoi un build voudrait le dépasser — c'est le contrat de T1-T3, pas un diagnostic des builds.
• --touch sur un module racine invalide toute la cascade aval : dimensionner --timeout à la cascade visée (mesuré : 47 modules + jumeaux _en > 30 min sous -Kjobs=5) ou toucher des feuilles.

Conformité

• §A : un sujet (le harnais de validation T5a) — le harnais et ses tests appariés. Collecte CI automatique (scripts/tests est un répertoire dans l'invocation pytest de scripts-tests.yml:271, pas une liste explicite — aucun câblage à toucher).
• See #15666 (contribution partielle à l'epic : T5a livré, T5b résiduel documenté, T4 est feat(ci,#15666): T4 garde CI anti-invocation-directe lake (AST, allowlist, TRANCHE15) #16196).
• feat(ci,#15666): T4 garde CI anti-invocation-directe lake (AST, allowlist, TRANCHE15) #16196 (T4, OPEN) : fichiers disjoints (check_lake_direct_invocation.py, lake_direct_allowlist.json) — pas de conflit attendu.
• Preflight au moment du commit : gh pr list --search 15666 = feat(lean,#15666): T2 admission raffinie -- tree lease, file bornee, budget min-des-sources #16098/feat(lean,#15666): T3 backend epingle par lake -- premier-ecrivain proprietaire #16160/feat(ci,#15666): T4 garde CI anti-invocation-directe lake (AST, allowlist, TRANCHE15) #16196 (T2/T3/T4, aucun sur T5a) ; seul claim T5 = le mien (c.5679738618) ; lane sœur vérifiée.

🤖 Generated with Claude Code

[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-09-15) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=2 cap=2)
• GENRE-UNKNOWN : le genre canonise `feat` est hors enumeration close -- trou d'adjacence G-VAR-3, requalifier le genre dans le body (Un genre hors énumération passe silencieusement : canonicalize_genre le rend tel quel, aucun signal, adjacence G-VAR-3 inatteignable #12158)
• 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]

VERDICT: LGTM — harnais T5a lu en entier (harnais 455 l. + tests 262 l.), preuve-vive vérifiée de bout en bout.

Vérifications réelles (pas advisory) :

1. Imports sibling : scan_native_population (l.172), state_dir (l.104), config (l.713) existent bien dans scripts/lean/lean_exec.py sur main — l'import du harnais ne cassera pas à l'exécution réelle.
2. Preuve-vive CI : scripts-tests.yml déclenche sur paths: scripts/** (couvre les 2 fichiers du PR), checkout v4 complet, et la commande pytest inclut scripts/tests → le Scripts Tests (CPU) vert sur 89633a8c a réellement exécuté test_validate_bounded_load.py. Les tests échoueraient si evaluate() mentait : population hors cap citée, timeout DriveFS nommé, spawn étouffé, orphelins comptés, record stale rejeté — c'est un vrai garde.
3. Réconciliation record : _emit (lean_exec.py l.759) écrit status/cmd/orphans à chaque sortie — read_organ_record lit le bon format.
4. Sans deadlock : sortie organe vers fichier (pas PIPE non drainé), sonde daemon + join(timeout) rend la main — testé.

Réserve mineure (non bloquante) : organ_exit_code est enregistré mais n'est pas un critère dur. Si l'organe crash avant _emit (SIGKILL, traceback), last_run.json conserve le run précédent ; cmd identique (lake build) → record stale accepté et organ_postcondition peut PASSER sur le run d'avant. Fermeture possible : réconciliation par started_epoch > début harnais, ou critère dur organ_exit_code == 0. Fenêtre étroite (le mur du harnais couvre déjà le kill volontaire) — à traiter en follow-up, pas bloquant pour cette tranche.

[Hermes hermes-pr-review, cycle :13 15/09, host c92df397a786]

[myia-ai-01]

Approved at exact head 89633a8c12b72df32499cba7c6eca9e0c0b51577 after full review of the PR surface, implementation, tests, and current gates.

The bounded-load harness is scoped to two new files, its 17 contracts are collected by the successful Scripts Tests run on this head, and the failure signatures are discriminating rather than vacuous. The documented stale-record window remains a non-blocking follow-up: a future hardening should reconcile last_run.json with the current harness start or require organ_exit_code == 0.

The squash description must not claim that T2/T3 are already on main; #16098 and #16160 remain open. This wording correction is prepared for merge time and does not affect the implementation verdict.

No closing issue reference is present; #15666 remains open for later tranches.

[myia-ai-01]

Requesting changes at exact head 89633a8c12b72df32499cba7c6eca9e0c0b51577 after full review of the body, comments, reviews, complete diff, integration points on live main, tests, checks, and closing references.

Two fail-open paths contradict this harness's purpose and must be closed before merge:

1. scan_native_population() uses -1 when population is not measurable. evaluate() currently keeps those samples, so an all--1 run produces max_pop = -1 <= cap and marks population_cap PASS with zero valid measurements. Filter invalid measurements and fail the criterion when none remain; add a contract for this exact case.
2. read_organ_record() reconciles only cmd. If the organ crashes before _emit, a prior successful last_run.json for the same lake build command is accepted as evidence for the current run. Bind the record to this invocation using a fresh run_id or a recorded start timestamp at/after the harness start, and add a same-command stale-record false-negative test.

These are not optional hardening nits: both turn an unmeasurable or crashed run into a possible successful validation result. The existing approval on this head is superseded by this exact-head finding.

Please integrate current main (5a1989a92e2185678763a06a76032b7384cd70e5) with the fix, run the targeted suite and full collected Scripts Tests, then obtain fresh post-base gates and an exact-head review. Keep closingIssuesReferences empty; #15666 is a partial-tranche epic and must remain open.

[jsboige]

Addressed both fail-open paths at new head c6a3d4d13 (fixes a3bc4f962 + c6a3d4d13, merge f5106afcc).

1. population_cap fail-open (all -1) — evaluate() now filters invalid measurements (population < 0 = scan_native_population failure) and FAILs the criterion when none remain, citing valid/total counts: 0 mesure de population valide sur 5 echantillons (scan en echec) -- critere non verifiable. Mixed runs judge on the valid samples only, both counts cited (7 mesures valides / 8 echantillons). Contracts 18-19 (test_population_non_mesurable_ne_valide_rien, test_population_mixte_juge_sur_les_mesures_valides).

2. stale same-command organ record — the harness now captures known_run_ids() (preexisting last_run.json + live run registry runs/*.json) BEFORE launching, and read_organ_record(expected_cmd, pre_run_ids) rejects any record whose run_id is missing (older format = potential stale) or preexisting (crash before emit leaves the previous run's file, same lake build command). The organ generates a fresh uuid run_id per invocation, so a record that reached emit always carries an unknown id. Contracts 20-21 (test_read_organ_record_rejette_le_stale_meme_commande, test_known_run_ids_lit_aussi_le_registre_des_runs).

Post-base validation on 5a1989a92:

• targeted: pytest scripts/tests/test_validate_bounded_load.py → 21 passed (17 + 4 new)
• full collected Scripts Tests: python -m pytest scripts/tests/ → 5665 passed, 30 skipped, 5 xfailed in 775.90 s
• CLI smoke end-to-end (lake --version in a real lake under the organ): PASS 4/4, record=lu (fresh run_id accepted through the new gate), rc=0

closingIssuesReferences stays empty — #15666 remains open (T5a partial tranche). Exact-head re-review welcome.

🤖 Generated with Claude Code

[myia-ai-01]

Approving exact head c6a3d4d13ab2a01f4a3bb95d72c488402377dd4c after re-reading the complete repair surface and independently tracing both prior false-pass paths through the harness, tests, and current lean_exec.py organ contract.

The population cap now fails closed when every sample is invalid: invalid negative scans are excluded, an empty valid set makes the hard criterion false, and the new all-invalid contract asserts both the criterion and global verdict. Mixed populations are judged only on valid samples and report valid/total counts.

The organ record is now bound to the current invocation. Known run_id values are captured before launch from both last_run.json and the live-run registry; records with a missing or pre-existing id are rejected, so a crash before emission cannot reuse a same-command stale record. The new contracts distinguish stale, missing, fresh, and concurrently registered ids. Current main 5a1989a92e2185678763a06a76032b7384cd70e5 is integrated, the two-file delta is additive, file collisions are absent, and closingIssuesReferences is empty so #15666 remains open.

This approval lifts my stale CHANGES_REQUESTED on 89633a8c12b72df32499cba7c6eca9e0c0b51577. Merge remains blocked until the current-head Scripts Tests CPU run, ADK contracts, and PR gate complete successfully; the author's local full-suite result is not a substitute for those gates.

[jsboige]

[ADJOINT PREFLIGHT] PR #16299 -- verdict: PREFLIGHT_HOLD (nits OK, mss=BLOCKED sans cause technique)

c.32 21:30Z UTC. État mesuré firsthand c.32 (Tell c.32-L1 ★★★ fondateur):

• main HEAD: 7885a69 (137 -> 138 PRs ouvertes depuis 21:21Z, +1 PR reviewée entre temps)
• pool c.32 21:30Z: 138/138 PRs ouvertes, 97/138 sans reviewDecision, 5/138 APPROVED actives
• target feat(lean,#15666): T5a validation charge bornée — harnais de sondes pendant un build lake réel sous lean_exec #16299: T5a validation charge bornée Lean harnais sondes, head=c6a3d4d13ab2, base=5a1989a92e21
• mss=BLOCKED, mergeable=MERGEABLE, reviewDecision=APPROVED, +843/-0 (gain de capacité net)
• stagnation feat(lean,#15666): T5a validation charge bornée — harnais de sondes pendant un build lake réel sous lean_exec #16299: 2 jours 2h 10min (updatedAt 2026-09-16T19:20:04Z, le +stagnant des 5 APPROVED)

B.0 organe canonique (Tell c.29-L3 ★★ parade §1):

• git rev-parse origin/main = 7885a69
• python check_unaddressed_nits_origin_main.py 16299 = exit 0 OK (0 nit non levé)
• 1 commentaire non-évalué postérieur au dernier commit: jsboige 2026-09-16T19:09:38Z (réparation fail-open paths)

Lecture 4 surfaces Tell c.28-L1 ★★★ EXHAUSTIF:

1. mss=BLOCKED : 3 checks failed au moment de la stale-mesure (ré-exécution en cours post-rien)
2. mergeable=MERGEABLE : pas de conflit git
3. reviews[].state=APPROVED : 1 review APPROVED (jsboige lui-même)
4. reviews[].body : LGTM sans réserve (PR mergée-candidate)

Hold = le mss=BLOCKED n'a pas de cause technique visible (code sain, 0 nit non levé, APPROVED granted) — c'est probablement un check stale qui se résoudra au prochain rerun, OU un job qui a timeout sans conclusion visible. Recommandation ai-01 : relancé une fois, et si mss reste BLOCKED sans cause technique investiguer en deeper (cf. #16643 slot WSL plafonné 3 GiB instance class). Si mss redevient CLEAN après rerun = MERGE_READY parfaite (la +substantielle des 5 APPROVED).

Tell c.1502 ××131ᵉ strict single-lane OK: 0 merge / 0 close / 0 CHANGES_REQUESTED par adjoint — commentaire only.

Grain: MED/coordination-watchdog.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16299
head: 48cec91
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 4
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: eec138e1f5569dd5821e9ffc0d0ff5ea58f8795a539e9770a09c6cd88406fdaf
diff-files: 2
diff-additions: 843
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]